北京
2025年底，數學圈出了一個很有傳播性的故事。
數論學家Ken Ono離開弗吉尼亞大學，加入硅谷AI初創公司Axiom Math。Ono做過美國數學會副主席，長期研究拉馬努金和數論。按傳統路徑，他本來應該繼續待在大學、研究所和講臺上。
Axiom Math由Carina Hong創辦。Hong當時24歲，MIT數學和物理本科出身，后來進入斯坦福讀博，又離開學校創業。她想做一個AI數學家：能解決數學難題，能生成證明，也能檢查自己的推理是否正確。
這也是這個故事最抓人的地方：一位資深數學家，加入了一位年輕創業者剛剛成立的AI數學公司。放在幾年前，這樣的組合很難想象。
Axiom的大目標，已經越過了讓模型算題、寫答案這一步。它要讓AI學會做可靠的數學證明，把證明寫進形式化系統里，讓機器能檢查每一步到底成立不成立。
幾個月后，資本市場也投了票。2026年3月，Axiom拿到2億美元A輪融資，估值約16億美元。一個剛成立不久的AI數學公司，靠“數學證明”講出了獨角獸故事。
最近幾年，AI在語言和圖像、視頻上都有了重大的突破。但是在數學上，AI的表現如何呢？數學不像寫文案、畫圖、做視頻。一個證明要么對，要么錯。錯一步，后面再漂亮也沒用。數學給AI提供了一把很硬的尺子。
如果AI只能寫出“看起來像證明”的文字，那它離真正的數學還很遠。只有當它能在這把尺子下面站住，我們才有資格繼續追問更大的問題。
所以問題來了：AI能不能發現新的數學定理？它是在做更快的計算器，還是已經開始碰到人類創造知識的邊界？
一、AI 一開始就是從數學證明里長出來的
1.1 第一個 AI 程序就在證明定理
很多人以為AI是最近幾年才開始碰數學，其實剛好反過來。AI這個學科最早的代表作品之一，干的就是數學證明。
故事要從1950年代的RAND公司講起。
那時候還沒有“人工智能”這個正式學科。有三個學者在RAND湊到了一起：Allen Newell研究組織和決策，Herbert Simon研究人怎樣在有限信息下做選擇，Cliff Shaw負責把這些想法寫成真正能跑的程序。
Newell和Simon關心的問題很直接：人類解決問題的時候，到底在做什么？如果一個人能一步步推理、排除、搜索、試錯，那么機器能不能也這么做？
他們挑的第一個靶子，是羅素和懷特海的《數學原理》。三卷本的《數學原理》是20世紀數學基礎研究里最有名的著作之一，試圖把數學建立在形式邏輯之上。書里的命題寫得非常嚴格，對機器來說正好合適：規則清楚，目標明確，每一步能不能走下去都可以檢查。
1955年底到1956年初，Logic Theorist的雛形做出來了。最有意思的是，最早的版本并不是直接在電腦上跑出來的。Simon后來回憶，他們把程序步驟寫在卡片上，讓家人和研究生分別扮演程序里的不同部件，像一臺“人肉計算機”一樣模擬程序運行。
這聽起來很原始，但它抓住了AI最早的核心想法：智能可以被拆成符號、規則和搜索。
等Shaw把程序真正搬到RAND的計算機上之后，Logic Theorist開始證明《數學原理》第二章里的定理。它最后證明了前52個定理中的38個。一個亮點是，有些證明比原書還短。
1956年夏天，Dartmouth會議召開，“Artificial Intelligence”這個詞在那里被正式推上臺面。Newell和Simon帶著Logic Theorist去參會。別人還在討論機器智能應該是什么樣子，他們已經拿出了一個會證明定理的程序。
所以AI從誕生第一天起，目標就不只是模仿人類輸出。它一開始想做的，就是邏輯推理，就是數學證明，就是讓機器進入人類最硬的智力活動之一。
1.2 希爾伯特的夢被打碎，但工具留下了
再往上追，故事會回到希爾伯特。
20世紀初，數學家已經擁有了微積分、集合論、非歐幾何、抽象代數，工具越來越強，地基卻越來越讓人不安。集合論里出現了悖論，幾何不再只有歐幾里得一種，分析學也剛剛經歷嚴格化。數學家突然意識到：我們每天都在證明定理，但“證明”本身到底有多可靠？
希爾伯特的回答很硬。他希望把整個數學變成一套可以機械檢查的符號系統。所有概念先清楚定義，所有推理都按規則展開，只要給出一個命題，原則上就能判斷它是真的、假的，還是能不能從公理里推出來。
這就是后來所謂的希爾伯特綱領。它有兩個核心愿望：第一，數學不能自相矛盾；第二，數學證明應該能被有限、明確、可檢查的規則管住。換句話說，數學不應該只靠大師的直覺和讀者的信任，它應該像一臺嚴密的機器。
這個夢想非常誘人。它等于給數學找一張最終安全證書：只要公理系統是安全的，所有在里面推出的定理就都是安全的。羅素和懷特海寫《數學原理》，也可以放在這條大線里理解。
然后，1931年，哥德爾來了。
哥德爾不完備定理把希爾伯特最樂觀的部分打碎了。他證明，在任何足夠強、足夠一致的形式系統里，總會存在一些真命題，無法在這個系統內部被證明。更麻煩的是，這個系統也無法用自己的力量證明自己的一致性。
這句話聽起來抽象，意思卻很重：數學不可能被完全壓成一臺萬能判定機。你不能指望有一套終極規則，把所有數學命題都自動判定完。
但希爾伯特的計劃并沒有完全白費。
哥德爾打碎的是“全自動解決一切”的終極幻想，不是形式化本身。恰恰相反，形式邏輯、證明論、可計算性理論、類型論、自動定理證明，后來都從這條線長出來。它們承認數學不可能被徹底機械化，但仍然努力把能機械化的部分盡量機械化。
AI的早期幾十年，尤其是所謂GOFAI，也就是Good Old-Fashioned AI，本質上大量依賴符號、規則、搜索和邏輯。Logic Theorist能出現，背后就有這條形式化傳統。今天的工具LEAN、Coq、Isabelle，也是在這條路上繼續往前走。
1.3 從神經網絡繞了一圈回到原點
按照1950年代那批人的想法，AI本來應該沿著邏輯和證明一路往前走。機器會推理，會搜索，會證明定理，再往前一步，也許就能理解自然語言、規劃行動、解決科學問題。
現實沒有這么順。符號AI很快撞到墻。手寫規則太脆，真實世界太亂，常識太多，例外也太多。一個小小的場景變化，就可能讓精心寫好的規則失效。到后來，符號AI給人的感覺越來越像一座漂亮但難維護的宮殿：邏輯上很干凈，走出實驗室就漏風。
然后神經網絡起來了。
它走的是另一條路：少寫規則，多喂數據。圖像識別、語音識別、機器翻譯、自然語言生成，都是這條路上打出來的勝仗。以前AI研究者想教機器“貓是什么”，現在直接給它看幾千萬張圖。以前想手寫語言規則，現在讓模型從海量文本里自己學。
這條路線太成功了，以至于很多人開始相信：智能不需要顯式規則，只要模型夠大、數據夠多、訓練夠狠，它就能自己長出來。符號、邏輯、證明這些老詞，突然顯得又慢又土。
但數學證明沒有那么容易被繞開。
你可以用神經網絡寫一段“很像證明”的文字，但數學不會因為它像就放行。證明需要每一步都成立，需要變量、定義、定理、前提條件全部對上。這里的麻煩，恰好是符號系統最擅長處理的東西。
所以現在劇情又繞回來了，而且不是一個實驗室在自嗨。
Google DeepMind在做AlphaProof，把AlphaGo、AlphaZero那套神經網絡加搜索的思路，搬進形式化數學證明。Harmonic在做Aristotle，目標是讓模型直接產出能被LEAN檢查的證明。Axiom Math押的是另一條更商業化的線：如果未來AI會寫大量代碼和科學推理，那么數學證明就可以變成驗證這些輸出是否可靠的工具。
這些項目的技術細節各不相同，但底層結構很像：用神經網絡猜路，用強化學習和搜索擴大嘗試范圍，再用形式化系統驗算。機器先提出可能的證明路徑，LEAN這類系統負責一行行檢查。猜錯了就退回去，猜對了才算真正往前走。
繞了70年，AI又回到Logic Theorist的出發點。區別在于，這一次它手里多了算力、數據、強化學習，還有LEAN這樣的形式化地基。
二、LEAN: 這場游戲的地基
2.1 LEAN 是檢查證明的機器
要理解AI證明數學，先要理解LEAN。
LEAN本身是一個定理證明器，也可以理解成一種極其嚴格的數學編程語言。它不負責和你聊天，也不負責替你“發揮”。你在LEAN里寫的是定義、命題和證明。
普通數學證明寫在紙上，靠同行閱讀、審稿和學術共同體來判斷對錯。人類寫證明時，經常會說“顯然”“由標準結論可知”“不難推出”。這些話在論文里可以成立，因為讀者默認作者和審稿人知道中間省略了什么。
LEAN不接受這種省略。
你在LEAN里寫一步，它就檢查一步。變量類型對不對，前提條件有沒有給齊，調用的定理能不能用，目標有沒有真的被證明完，它都會檢查。只要LEAN接受，這個證明就在它的公理系統和庫依賴下成立。它不看文風，不看氣勢，也不看作者名氣。
所以你可以把LEAN想成數學世界里的編譯器。
寫程序時，編譯器不關心你覺得代碼“應該能跑”。它只看語法、類型和規則。LEAN也是這樣。你說“顯然可得”沒有用，除非你把“顯然”的每一步都寫清楚，或者調用庫里已經證明過的定理。
這就是LEAN和ChatGPT式數學輸出的根本差別。ChatGPT可以寫出一段很像證明的文字，讀起來順，但中間可能有坑。LEAN里的證明要么通過檢查，要么報錯。它把“像不像證明”變成了“是不是證明”。
2.2 Leonardo de Moura 為什么要做 LEAN
LEAN的核心人物是Leonardo de Moura。他是微軟研究院的研究員，長期做自動推理和形式化驗證。
他更早的代表作之一是Z3，微軟研究院開發的SMT求解器。SMT求解器可以理解成一種自動邏輯工具，擅長在很多約束條件里判斷是否存在解，廣泛用在程序驗證、硬件驗證和軟件工程里。
但自動工具有一個問題：它們很強，也很黑箱。你把問題丟進去，它給你答案；可是一旦問題變得非常抽象、非常數學化，人還是需要參與構造證明。傳統交互式證明器正好相反，人可以一步步寫證明，但自動化又經常不夠順手。
LEAN想把這兩邊接起來。
2013年，de Moura在微軟研究院啟動LEAN項目。官方Reference里寫得很清楚：LEAN的目標，是把一個很小、可以獨立實現的可信邏輯內核，和SMT求解器這類自動化工具的便利性結合起來，同時能擴展到大問題。
這句話翻成白話就是：底層要足夠小，才能讓人相信；上層要足夠好用，數學家和程序員才愿意真的寫東西。
2015年，de Moura、Soonho Kong、Jeremy Avigad、Floris van Doorn和Jakob von Raumer在CADE會議上發表了LEAN的系統論文。那篇論文把LEAN定義為一個開源定理證明器，使用基于依賴類型論的小型可信內核，目標是連接交互式證明和自動證明。
這也是LEAN后來能長大的關鍵。它一開始就沒有只想做一個學術玩具，而是想做一個平臺：可以寫數學，可以做軟件驗證，可以做教育，也可以讓自動化工具嵌進來。
2.3 從 LEAN 3 到 LEAN 4：從證明器變成語言
LEAN最早的版本更像研究原型。
官方歷史里寫到，LEAN 0.1在2014年6月發布。早期版本主要以C++庫的形式存在，讓其他程序可以調用它來構造可檢查的證明。后來，LEAN逐漸往傳統交互式證明器演化，先有Lua寫的tactic，再有專門的前端語法。
2017年1月，LEAN 3發布。對數學社區來說，這是一個關鍵節點。LEAN 3足夠穩定，也足夠可擴展，數學家開始認真拿它干活。更重要的是，它支持很強的自擴展能力：tactic、記號、頂層命令，都可以用LEAN自己定義。
這聽起來像語言設計細節，其實影響很大。數學不是一套固定格式。代數有代數的寫法，拓撲有拓撲的寫法，范疇論有范疇論的寫法。如果一個證明器不能讓社區自己擴展語言和工具，它很難承載現代數學的復雜表達。
LEAN 3的成功也帶來一個問題：系統本身主要還是C++實現，擴展起來有成本。于是LEAN 4開始重寫。
2018年，LEAN 4開發啟動。2023年9月，LEAN 4.0正式發布。它是新版證明器，也是一門更完整的函數式編程語言。官方Reference里說，到了LEAN 4，大約90%的LEAN實現代碼本身用LEAN寫成，也就是所謂self-hosted。
這里很容易誤解。LEAN 4不是一個“把人類證明自動翻譯成機器語言”的轉換器。它更像一個數學證明的編程環境：你在里面定義對象，寫下命題，再把證明寫成一行行代碼。LEAN 4負責檢查這些證明代碼是否真的成立。
把自然語言證明翻譯成LEAN代碼，是另一個問題，叫autoformalization。比如論文里寫“顯然，由緊性可知存在有限子覆蓋”，翻成LEAN時，你要說明空間類型、緊性的定義、開覆蓋怎么表示、調用哪個已有定理。翻譯完以后，LEAN 4還要繼續檢查它。
這一步很重要。它意味著LEAN不再只是“檢查數學證明的工具”，也變成了“寫工具的工具”。用戶可以更方便地做自定義語法、自動化tactic、領域專用工具。對AI證明數學來說，這一點尤其關鍵，因為AI不只需要一個判卷老師，還需要一個可以嵌入搜索、生成、反饋和自動化的環境。
2.4 mathlib 是 AI 數學的工具箱
真正讓LEAN變成AI數學基礎設施的，是mathlib。
mathlib是LEAN社區維護的數學庫。它的目標很樸素，也很瘋狂：把盡可能多的現代數學，翻譯成機器可檢查的定義、定理和證明。
一個證明器本身再漂亮，如果沒有庫，也很難做事。就像你寫程序，不會每次都從零實現數組、哈希表、網絡協議和文件系統。數學也是一樣。你要證明一個數論命題，可能要用群、環、域、拓撲、分析、組合、序理論、范疇論里的很多舊結論。沒有庫，每一步都要從公理開始，根本走不遠。
mathlib解決的就是這個問題。
它把代數、分析、拓撲、數論、組合、范疇論等大量數學內容，一條條翻譯成LEAN可以檢查的形式。這個工作非常慢，也非常苦。很多時候，一個人類論文里一句“由標準結論可知”，在LEAN里可能要展開成幾十行甚至幾百行代碼。
LEAN 3時代，mathlib已經積累到超過100萬行形式化數學。2023年，社區又把mathlib遷移到LEAN 4。官方Reference提到，遷移完成后，mathlib繼續增長到超過150萬行，而且LEAN 4檢查更大的庫，速度反而比LEAN 3檢查較小的庫更快。
這不是一個小工程。它更像把數學世界一塊塊搬進機器能讀的城市里。每搬進去一個定義、一個引理、一個定理，后面的人和AI就少走一步路。
所以AI數學這輪變化，底層并不只是“模型突然變聰明”。它是兩件事疊在一起：形式化社區先花多年修路，神經網絡再用搜索和訓練把這條路跑得更快。
2.5 為什么 AI 最終會盯上 LEAN
現在再回頭看，AI盯上LEAN并不奇怪。
大語言模型擅長生成候選答案，但它最大的問題是不可驗證。它可以寫出一段語氣很像數學家的證明，也可以一本正經寫錯。自然語言證明里有太多省略，普通讀者甚至很難看出錯在哪里。
LEAN給AI提供了一個罕見的訓練環境。
模型每寫一步證明，LEAN都能給出干凈反饋：通過，或者不通過。這個反饋非常適合搜索和強化學習。模型可以先猜一個證明步驟，LEAN檢查；失敗就換路，成功就繼續。成功路徑還能變成新的訓練數據。
這就是為什么DeepMind、Harmonic、Axiom這些玩家都繞不開LEAN和mathlib。DeepMind需要一個可驗證的競賽數學環境，Harmonic需要證明文件真正通過檢查，Axiom需要把數學證明變成代碼和科學推理的可信底座。
換句話說，LEAN不是AI數學故事里的配角。它更像這場游戲的地基。沒有它，模型只能生成“看起來像證明”的文字；有了它，AI才有機會把猜想、搜索和驗證連成一個閉環。
三、現在的玩家已經不只是實驗室
3.1 DeepMind 把 IMO 變成公開靶場
2024年7月，Google DeepMind把這個方向推到大眾視野里。它沒有先去宣布“AI要解決黎曼猜想”，而是選了一個所有人都看得懂的靶場：國際數學奧林匹克競賽，IMO。
IMO有兩個好處。第一，題目足夠難，全世界最強中學生都在這里競爭。第二，規則很清楚，滿分42分，6道題，每道7分，最后可以直接和人類選手比較。對AI來說，這是一個天然的公開benchmark。
DeepMind發布的系統叫AlphaProof和AlphaGeometry 2。前者主攻代數、數論這類可以走形式化證明路線的問題；后者主攻幾何。兩個系統合起來，在2024年IMO上解出6道題中的4道，總分28分，達到銀牌上沿。那一年金牌線是29分，它離金牌只差1分。
這件事真正刺激人的地方，不只是“AI會做奧數題”。更關鍵的是，AlphaProof走的是形式化證明路線。它把自然語言問題轉成形式化表達，再用強化學習和搜索去找證明，最后讓證明系統檢查。DeepMind等于把AlphaGo、AlphaZero那套“神經網絡加搜索加強化學習”的結構，搬到了數學證明里。
這和普通模型寫一段漂亮證明完全不同。普通模型可以胡說，AlphaProof要讓機器驗算。它做出來的東西，至少要在形式系統里站得住。
但這里也要潑一盆冷水。IMO金牌級不等于研究級數學家。
競賽題是人為設計的封閉問題，條件清楚，目標明確，答案一定存在。研究級數學經常連正確問題是什么都不清楚，更不用說把它翻譯成LEAN里的精確定義。真正的數學研究還需要選題、定義、品味、背景判斷和長期的理論積累。
3.2 Harmonic 和 Axiom 把數學證明做成公司
DeepMind的意義，是證明這條路能打公開比賽。Harmonic和Axiom的意義，是把這條路做成公司。
先看Harmonic。
Harmonic由Tudor Achim和Robinhood聯合創始人Vlad Tenev創辦。它對外講的詞很大，叫Mathematical Superintelligence，數學超級智能。這個詞當然有營銷成分，但它背后的問題很具體：如果AI經常幻覺，能不能用數學證明把它按住？
Harmonic的核心產品叫Aristotle。到了2025年，Aristotle在IMO方向又往前走了一步。Harmonic官方披露，Aristotle在2025年IMO上達到金牌級表現，形式化解決了6道題中的5道，并開源了部分LEAN證明文件。它的技術報告里也明確說，只有系統產出完整的LEAN 4證明，而且沒有sorryAx這類不可靠占位，才算真正解決。
這個標準很硬。很多系統做數學題，是寫出一個看起來合理的解答。Aristotle要交的是可以被LEAN檢查的證明文件。一個占位符、一個沒有補完的證明洞，都不能算數。
資本也迅速跟上。Harmonic 2025年11月宣布完成1.2億美元Series C，估值14.5億美元。它已經是一家圍繞“可驗證數學推理”融資、招人、做API的AI公司。
另一個明星公司是Axiom Math。Axiom由Carina Hong創辦，2026年3月，Menlo Ventures宣布領投它2億美元A輪，投后估值16億美元。
Axiom的招人故事也很有傳播性。Ken Ono，這位數論領域的知名數學家，離開弗吉尼亞大學的學術崗位加入Axiom，擔任founding mathematician。一位資深數學家加入年輕創業者創辦的AI數學公司，本身就足夠抓眼球。
那Axiom到底做什么？
它的目標不是做一個“會聊天的數學模型”，也不只是幫數學家證明幾個漂亮定理。Axiom押的是Verified AI，也就是可驗證的AI。它要讓模型生成的東西，最后能被形式化證明檢查。
最直接的場景是代碼。未來AI會寫大量代碼，但“能跑”“通過測試”“看起來沒問題”都不等于安全。金融交易、加密協議、自動駕駛、醫療系統、AI基礎設施里的代碼，錯一次代價可能很高。Axiom想做的，是讓AI寫出來的關鍵代碼和關鍵推理，能夠被數學證明驗證：這個函數對所有輸入都返回正確結果，這段邏輯不會破壞數據，這個系統不會引入某類安全漏洞。
所以Axiom的商業敘事不是“數學家失業”。它更像是在給AI生成代碼和AI推理加一層可信度。AI負責生產，Axiom負責證明這些輸出真的符合規格。
Axiom自己也在做工具層。它公開的AXLE，也就是Axiom LEAN Engine，提供的是探索、驗證、操作數學證明的交互式工具。你可以把它理解成Axiom內部訓練和驗證系統的一部分：模型生成證明，AXLE/LEAN這類工具負責檢查、提取定理、操作證明對象。
所以Harmonic和Axiom看起來都在做AI數學，側重點并不一樣。Harmonic更像從數學推理模型往外擴，Axiom更像從可信AI和代碼驗證往里打。它們共同說明一件事：數學證明已經從學術實驗，變成了AI創業公司的核心敘事。
3.3 錢開始流向基礎設施，但研究級數學還很遠
與此同時，錢也開始進入基礎設施層。
這一點很重要。真正推動AI數學的，不會只有幾家閉源公司。它還需要數據集、形式化庫、autoformalization工具、LEAN教學、現代定理形式化項目。換句話說，它需要一整套公共基礎設施。
XTX Markets和Renaissance Philanthropy就是這一層的代表。AI for Math Fund最初由XTX Markets支持，后來擴大到1800萬美元，資助29個項目。2026年3月，Renaissance Philanthropy和XTX又宣布追加1350萬美元，把總承諾提高到3150萬美元。
這些錢投向的東西很具體：形式化數學數據集，autoformalization工具，LEAN教學，把現代數學定理搬進形式化庫。比如有項目要把頂級數學期刊里的現代定理形式化出來，有項目要做本科生證明的自動形式化和反饋工具。
這里還必須提一個開源項目：LeanDojo。
LeanDojo由Caltech、NVIDIA、MIT等機構的研究者在2023年推出，論文發表在NeurIPS 2023。它解決的是一個很工程、但很關鍵的問題：機器學習模型怎么和LEAN交互？如果每個團隊都自己寫一套抽取數據、運行證明、記錄狀態、評測結果的工具，這個領域很難復現，也很難積累。
LeanDojo做了兩件底層工作。第一，它從LEAN和mathlib里抽取證明數據、proof state、tactic和premise信息，做成可以訓練模型的數據。第二，它把LEAN變成一個類似gym的交互環境：模型可以看到當前證明狀態，提交下一步tactic，LEAN返回成功、失敗或新的子目標。
它還提出了ReProver，一個帶檢索的證明模型。這個思路很自然：證明一個定理時，模型不能只靠自己背下來的參數，它還要從龐大的數學庫里找可能用得上的舊定理。LeanDojo論文里構造了接近10萬個來自mathlib的定理和證明，用來訓練和評測這種檢索增強的證明器。
所以LeanDojo的意義，不在于它自己是不是最強的數學AI。它更像一個開放訓練場，把“模型如何讀LEAN、如何和LEAN互動、如何從mathlib里找工具”這件事標準化。后來的很多AI證明工作，都離不開這種基礎設施。
陶哲軒（Terence Tao）也在這個基金的顧問名單里，并多次公開談到AI和LEAN對數學協作的潛力。他的態度很有代表性：AI短期內不是按一下按鈕就吐出深定理的神機，更像一個能幫數學家查庫、補引理、找邊界、整理證明的協作工具。
這說明AI數學已經過了“幾個研究員做benchmark”的階段。大廠、創業公司、VC、交易公司、慈善基金、數學家，都開始把它當成一條可能改變科研和軟件工業的基礎路線。
四、AI 到底怎么證明一個定理
4.1 AI 負責猜，LEAN 負責判
AI證明數學的核心結構，可以壓成一句話：AI猜，LEAN判。
想象你給系統一個命題：證明某個數論結論，或者證明某段代碼滿足某個規格。第一步是把目標放進LEAN這樣的形式化環境里，而不是先寫一段漂亮解釋。系統要知道對象是什么，變量是什么，前提是什么，最后要證明的目標是什么。
然后模型開始猜路。
它讀過大量數學材料和LEAN代碼，學過命題怎么寫、定義怎么展開、證明套路怎么走、tactic怎么用。面對一個新目標，它可能先生成一個證明步驟，也可能先拆出幾個中間引理。比如先證明一個更小的等式，再把這個等式接回原目標。
LEAN做另一件事。它不負責靈感，不負責猜路，只負責驗算。模型寫出一行LEAN證明，LEAN檢查這行是否成立。通過就進入下一個狀態，不通過就報錯。
這就像一個人負責想下一步棋，另一個裁判負責判斷這步棋合不合法。AI的價值在于提出候選路徑，LEAN的價值在于保證每一步沒有偷渡。
4.2 它和 ChatGPT 寫證明不是一回事
這和普通ChatGPT寫數學證明差別很大。
ChatGPT可以寫出一段非常像人類論文的證明。它會說“由緊性可知”“顯然存在”“不難推出”，讀起來很順。但只要中間某個“顯然”其實不成立，整段文字就塌了。更麻煩的是，很多讀者看不出來它塌在哪里。
LEAN不吃這一套。你不能用語氣騙過它。一個變量類型不對，一個條件沒傳進去，一個定理適用范圍不滿足，它都會報錯。AI在LEAN里寫證明，等于每一步都要過安檢。
舉一個很小的例子。人類論文里寫“由緊性可知存在有限子覆蓋”，讀者大概能懂。但在LEAN里，這句話要變成一串明確操作：當前空間是什么類型，緊性定義調用哪一個，開覆蓋如何表示，有限子覆蓋是哪個對象，用哪個已有定理把它拿出來。
如果其中一個對象類型不對，LEAN就不會讓你往下走。它不會因為這句話“數學味很足”就放行。
所以普通模型寫證明，是在生成一段像證明的文本。AI加LEAN寫證明，是在生成一段會被機器逐步檢查的證明代碼。這兩件事差別很大。
4.3 檢索舊定理，生成下一步 tactic
真正的證明很少從零開始。
數學家做證明，也會先想：這個問題像不像某個已知定理？有沒有可以調用的引理？這個結構是不是應該用緊性、完備性、歸納法、同構、范疇論里的某個標準工具？
AI也要做類似的事。它不能只靠參數里“記住”的數學知識。mathlib太大了，定理太多了，很多時候關鍵不在于模型會不會寫下一行，而在于它能不能找到該用哪一個舊定理。
這就是LeanDojo和ReProver那類工作的意義。模型看到當前proof state以后，先從mathlib里檢索可能有用的premise，再把這些候選定理和當前目標一起喂給模型，讓它生成下一步tactic。
Tactic可以理解成LEAN里的證明動作。它可能是“用這個定理改寫目標”，可能是“把目標拆成兩個子目標”，可能是“對自然數做歸納”，也可能是“把某個條件交給自動化工具處理”。每走一步，LEAN都會返回新的proof state。
于是證明過程變成一棵搜索樹。一個目標可以往很多方向走，有些方向馬上報錯，有些方向走幾步才死，有些方向能把目標拆小，最后一路走到所有子目標都被解決。
4.4 強化學習吃到了干凈反饋
這個結構特別適合強化學習。因為LEAN給出的反饋非常干凈：通過，或者不通過。沒有“看起來還行”，沒有“老師給你5分辛苦分”。模型可以在LEAN環境里反復嘗試，把成功路徑當成訓練數據，把失敗路徑丟掉或修正。
這也是為什么DeepMind那批做過AlphaGo、AlphaZero的人會撲向數學證明。圍棋有一個規則明確的棋盤，走法對錯和勝負可以被系統判定。形式化數學也有一個規則明確的符號世界，證明是否成立可以被LEAN判定。
但數學比圍棋麻煩得多。
圍棋棋盤有限，規則固定，目標就是贏。數學里的“下一步該引入什么定義”“該證明哪個引理”“這個問題應該放進哪個理論框架”，沒有那么清楚。證明空間大得離譜，很多時候連搜索方向都需要人類數學直覺。
所以現在的系統通常不會只靠模型一次生成完整證明。它更像是在一個形式化環境里反復試：生成若干候選tactic，LEAN檢查，保留能推進的路徑，失敗的路徑回退。搜索算法負責在許多候選路徑之間分配計算資源，模型負責提出更可能有用的下一步。
一旦某條路徑最終通過，系統就得到一個干凈樣本：這條證明是真的。這個樣本可以繼續拿來訓練模型。失敗路徑也有用，因為它告訴模型哪些操作不該在類似狀態下使用。
這就是AI證明數學吸引人的地方。它不像寫文章那樣很難判分，也不像很多科學實驗那樣反饋慢。形式化證明給了模型一個快速、明確、可重復的訓練信號。
4.5 Autoformalization 是最硬的瓶頸
所以現在最難的瓶頸之一，是autoformalization。
這個詞指的是把人類自然語言寫的數學，自動翻譯成LEAN里的形式化表達。它包括兩層：把命題翻譯成LEAN里的精確定義，也把證明翻譯成LEAN可以檢查的步驟。
它難在好幾層。
第一層是省略。比如論文里寫“令X為緊Hausdorff空間”，LEAN需要知道你調用的是哪個拓撲結構、哪些實例、哪些已有定理。論文里寫“由標準結論可知”，LEAN要知道這個標準結論到底是哪一個定理，前提條件是否滿足，變量如何對應。
人類數學家默認共享的大量背景，在機器眼里都要顯式寫出來。
第二層是概念選擇。同一個數學對象，可以用不同方式形式化。一個群作用、一個拓撲空間、一個范疇里的對象，放進LEAN時要選哪套定義？選錯了，后面可能每一步都很難走。人類數學家會憑經驗選擇最順的語言，機器現在還不穩定。
第三層是庫映射。自然語言里一句“用Hahn-Banach定理”，到了LEAN里不一定剛好有一個同名定理可以調用。庫里的定理可能叫另一個名字，前提寫法可能不同，結論形式也可能差一點。模型要找到能用的版本，還要補齊中間轉換。
第四層是證明重構。人類證明經常只寫主線，把大量計算、邊界條件和小引理留給讀者。LEAN不會替你腦補。很多時候，原論文的一段證明，形式化時要拆成一串新的lemma，證明順序也要重排。
最難的一層是上下文。論文里的一個符號，可能依賴前面幾十頁的約定；一個“顯然”，可能依賴作者所在領域的默認技巧；一個“標準構造”，可能根本沒有寫出來。autoformalization真正要處理的，是整篇論文背后的數學語境。
如果autoformalization做通，AI數學會發生質變。過去一百年的論文、教材、講義和證明，都可以更快進入機器可驗證的世界。AI不再只是在mathlib里玩，它可以真正讀懂數學文獻的骨架。
但這一步現在還遠遠沒完全解決。自然語言數學太省略，庫里的形式化表達又太精確。把它翻成LEAN，需要做的遠超語言轉換，更像是把一篇論文重新拆成定義、引理、依賴關系和可檢查步驟。
五、VC 砸錢賭的不是黎曼猜想
5.1 數學定理本身很難賣錢
很多人看到Axiom、Harmonic的估值，會本能地問：證明數學定理怎么賺錢？
答案很直接：很難靠數學定理本身賺錢。
如果某家公司明天證明了黎曼猜想，數學界會震動，媒體會刷屏，公司會收獲巨大聲譽。但這不是一個清晰的商業模式。沒有哪個客戶會因為你證明了黎曼猜想，每年給你付幾千萬美元訂閱費。
數學定理的價值很奇怪。它一旦被證明，就屬于全人類知識。你可以因為這個成果拿獎、拿名聲、拿學術地位，也可能因此吸引人才和資本。但它不像SaaS賬號，也不像API調用，很難按次收費、按席位收費、按年續費。
這也是為什么Axiom和Harmonic雖然講數學，但資本真正看的不會是“證明多少個漂亮定理”。漂亮定理是展示能力的舞臺，商業化要落到另一個問題：這些證明能力能不能變成別人愿意長期付費的可靠性服務？
換句話說，數學本身是招牌，驗證才是產品。
5.2 真正的市場在形式化代碼驗證
VC真正看上的，是形式化驗證。
AI寫代碼已經變成巨大市場。Cursor、Claude Code、GitHub Copilot、OpenAI Codex這類工具正在把代碼生產速度拉上去。問題是，AI寫的代碼經常有bug。有些bug只是頁面錯位，有些bug會變成安全漏洞、金融損失、自動駕駛事故或醫療系統錯誤。
傳統軟件工程靠測試。測試可以覆蓋很多情況，但它本質上是抽樣。你測了1000個輸入，也不能證明第1001個輸入不會出事。形式化驗證要解決的是另一類問題：在數學意義上證明這段程序滿足某個規格。
這里要把“測試”和“證明”的差別說清楚。
測試是在問：我試過這些情況，它們都沒壞。形式化驗證是在問：在某個精確定義的范圍內，這段程序對所有情況都滿足規格。前者是經驗保證，后者是數學保證。
舉個很小的例子。一個轉賬函數，測試可以檢查100美元、0美元、負數輸入、余額不足等很多case。形式化驗證想證明的是：不管輸入怎么變化，只要滿足前提條件，總金額不會憑空增加，賬戶余額不會變成非法狀態，權限條件不會被繞過。
這就是Menlo Ventures投Axiom時講的邏輯。Menlo的文章標題很直白：AI會寫所有代碼，數學會證明它能工作。它們押注的是一個未來：代碼越來越多由AI生成，真正稀缺的東西變成“可信”。
Menlo文章里有一句判斷很關鍵：AI生成代碼看起來對，能編譯，經常能跑，但這離“可證明正確”還很遠。它們認為這類問題來自統計模型本身，很難靠下一個模型版本自動消失。Axiom要做的，就是把AI代碼生成從“概率上靠譜”推進到“關鍵部分可以被數學證明”。
金融系統、加密協議、航空航天、自動駕駛、醫療設備、基礎設施軟件，這些地方錯一次代價很高。如果AI能把形式化驗證成本降下來，真正的市場會來自所有需要高可靠軟件的公司，數學家只是早期用戶。
Harmonic也在往這個方向走。它2025年12月發布Aristotle在VERINA Code Verification Benchmark上的結果，聲稱解決了189個形式化規格中的183個，完成率96.8%。這類benchmark的目標已經從數學競賽題轉向了代碼和規格的一致性驗證。
這說明數學證明能力正在外溢。先在IMO、Putnam、mathlib里證明自己能推理，再把同一套能力遷移到代碼驗證。真正的客戶不一定關心群論、數論和拓撲，但他們關心一件事：AI寫出來的關鍵代碼，能不能放心上線。
5.3 形式化驗證過去為什么沒火
問題是，形式化驗證不是新東西。
它已經存在幾十年，也確實有很多硬核成果。seL4微內核就是經典例子。它用形式化方法證明了操作系統內核的關鍵正確性和安全性質，被高安全系統反復引用。DARPA這些年也一直資助形式化方法，用在安全文檔解析、系統建模、高保證軟件等場景。
如果這東西這么好，為什么過去沒有大規模普及？
原因也很直接：太貴、太慢、太難用。
過去做形式化驗證，往往需要懂軟件工程、懂數學、懂邏輯、懂證明工具的人。這樣的人本來就少，還貴。很多時候，寫規格、寫證明、維護證明的成本，甚至比寫代碼本身還高。Menlo那篇文章提到傳統形式化驗證市場很小，一個原因就是它常常需要博士級專家，甚至可能出現“每一行代碼配很多行證明”的成本結構。
工程團隊也不喜歡這種工作方式。產品要上線，需求在變，代碼在改。只要代碼一改，證明可能也要跟著改。對大多數互聯網業務來說，測試、監控、灰度、回滾已經夠用了。它們寧愿承受一點線上bug，也不愿為數學意義上的正確付出巨大成本。
所以形式化驗證過去一直停留在高價值、高風險、強監管的地方。航空航天、軍工、加密、操作系統內核、金融基礎設施，這些地方值得做；普通業務系統大多不會做。
AI帶來的變量，是成本結構可能變了。
如果模型能自動寫規格、自動補證明、自動修復證明失敗的地方，形式化驗證的門檻就會下降。過去需要頂級專家做幾周的事，未來可能變成工程師點幾次、模型跑一會兒、系統給出證明和反例。
這正是Axiom、Harmonic這類公司最想講的故事：形式化驗證過去是少數專家手里的奢侈品，它們試圖把它變成AI時代的軟件基礎設施。
5.4 Agent 的信任層和估值泡沫
還有一層更大的想象空間，是AI agent的信任層。未來如果agent能替你轉賬、下單、改數據庫、部署代碼、簽合同，那么它每次行動前都需要某種可驗證約束。它不能只是“我覺得這樣沒問題”，它要能證明這一步不違反規則。
這就是數學證明技術可能商業化的地方。客戶不在數學系，而在軟件、金融、安全、機器人和AI平臺。
比如一個代碼agent要改支付系統，它最好能證明自己沒有改變金額守恒；一個數據庫agent要批量遷移數據，它最好能證明關鍵字段不會丟；一個交易agent要執行策略，它最好能證明不會突破風控限制；一個機器人agent要操作物理設備，它最好能證明某些安全邊界不會被越過。
這時候，證明技術就不只是“檢查代碼對不對”。它變成agent行動前的護欄。agent越能做事，驗證層越值錢。
但我對這里的估值仍然保持懷疑。
形式化驗證過去幾十年一直是好東西，但始終沒有大規模普及。大家知道它嚴謹，真正卡住普及的是貴、慢、難用，以及對工程團隊要求太高。AI可以降低門檻，但能不能降低到普通公司愿意買單，還沒有答案。
很多公司可能會選擇另一條便宜路線：更強的模型，加更多測試，加灰度發布，加監控回滾。它們不一定愿意為了“數學意義上的正確”多付幾十倍成本。只有當事故代價足夠高，或者監管要求足夠硬，形式化驗證才會從高級玩具變成預算項。
所以VC賭的不是“AI證明黎曼猜想后賣門票”。他們賭的是兩件事。
第一，AI生成代碼和agent行動會變得越來越多，風險也會越來越大。第二，AI本身能把形式化驗證的成本打下來。前者創造需求，后者降低供給成本。兩件事同時成立，這個市場才會打開。
如果只有前者，沒有后者，形式化驗證還是太貴。如果只有后者，沒有足夠高風險的應用，客戶也不急著買單。這就是這條賽道最核心的商業不確定性。
六、三年內能看到什么，別期待什么
6.1 幾乎確定：庫會變大，工具會進日常
未來三年，最確定的變化是mathlib會繼續長大。
這件事聽起來不刺激，但它最穩。AI for Math Fund、LEAN FRO、Harmonic的捐贈和贊助、大學里的形式化項目，都會把更多現代數學搬進LEAN。代數、分析、數論、拓撲、范疇論里還會有更多定義、定理和證明被寫成機器能檢查的形式。
這個過程很慢，但很扎實。每搬進去一塊，AI能使用的工具箱就大一圈。今天模型卡住，可能只是因為某個舊定理還沒進庫，或者進庫了但名字、形式、依賴關系很難找。三年后，這類低級摩擦會少很多。
第二個確定變化，是autoformalization會明顯進步。
它未必能一鍵把論文變成LEAN證明，但會先在更窄的場景里變好。比如把教材里的標準定理形式化，把本科生證明題翻成LEAN，把論文里的局部lemma翻成機器可檢查版本。這些小場景一旦跑順，就會慢慢擴大到更復雜的論文片段。
數學家也會越來越多地把AI當成日常工具。它不一定替你想出核心思想，但可以幫你查庫、補lemma、驗證邊界條件、找反例、把一個證明草稿改成更嚴謹的形式。陶哲軒談AI時更偏向這個方向：AI像一個能協作的初級助手，而不是按一下按鈕就給出深theorem的神機。
這種工具進入日常以后，數學家的工作方式會變。以前你要花一天查一個庫里有沒有某個lemma，以后可能幾分鐘就能問出來。以前一個證明草稿有一堆邊界條件，AI可以先幫你試著形式化，告訴你哪里少了前提。它像一個不知疲倦的研究助理，水平未必最高，但能不斷試錯。
高端軟件驗證也大概率會起量。金融、加密、航空、自動駕駛、醫療設備和AI基礎設施里，會有一批客戶愿意為更強保證付費。Axiom、Harmonic這類公司如果能先在這里落地，估值故事就不只是故事。
但這里的落地不會是全行業鋪開。更可能先從小模塊開始，比如關鍵函數、加密協議、智能合約、風控規則、數據庫遷移腳本、agent行動約束。先證明最危險的局部，再慢慢擴大。
6.2 可能發生：中等難度開放問題被 AI 補上
比較可能發生的標志性事件，是AI在某個具體子領域里解決一個有學術分量的開放問題。這個問題大概率不會是黎曼猜想那種全人類盯了一百多年的超級難題，而是某個邊界清晰、可以形式化、已有大量工具可用的中等難度問題。
這類問題有幾個特征。背景已經比較成熟，相關定義和定理大多能形式化；問題本身邊界清楚，不需要發明全新的語言；證明可能需要大量搜索、拆case、組合已有工具。人類數學家能看出方向，但細節太多，或者某個關鍵連接長期沒人撞上。
Axiom聲稱已經在類似方向上拿到過結果，Harmonic也在宣傳它解決過未解Erdos問題的形式化版本。哪怕對這些宣傳保持謹慎，也能看出方向：AI最先可能補上的，是那些“理論框架已有、證明空間巨大、需要大量試錯”的問題。
這類事件一旦發生，媒體標題一定會寫成“AI擊敗數學家”。真實情況會復雜得多。很可能是人類提出問題、整理背景、搭好LEAN環境，AI在其中補上關鍵證明或大規模搜索。它仍然值得重視，但不等于數學家失業。
更準確的說法，可能是“AI參與解決了一個開放問題”。人類負責選題、建模、解釋結果、檢查數學意義；AI負責在形式化空間里跑大量搜索，找到人類沒有及時發現的連接。
6.3 別期待：黎曼猜想級別還沒到時候
三年內基本別期待AI解決黎曼猜想、P vs NP、Navier-Stokes這種級別的問題。
這些問題難在需要新的概念、新的語言、新的理論框架，單純加算力和數據很難解決。人類數學史上真正的大突破，往往不靠把舊工具用得更快，而靠發明新的看法。AI現在更像一個極強的證明搜索和形式化工具，還不像一個能獨立發明新數學語言的研究者。
超級難題還有一個現實問題：它們周圍的形式化基礎不一定夠。你要讓AI解決黎曼猜想，不只是把一句“證明黎曼猜想”丟給模型。你需要把相關的解析數論、復分析、譜理論、代數幾何或者其他可能路線，盡量放進可用的形式化環境里。這個地基本身就是巨大工程。
而且超級難題通常需要新的結構，單純長計算不夠。人類歷史上的大定理，很多時候靠的是換一張地圖，舊路加速只能解決一部分問題。AI能不能發明這種地圖，現在還沒有證據。
所以三年內更現實的邊界是：AI在已有理論框架里變得很強，在形式化證明搜索里變得很強，在局部引理和中等問題上越來越有用。但“獨立發明新數學語言、解決最頂級難題”，還不是當前最該下注的預期。
6.4 公司結局：大廠收購會比數學突破更早
公司層面倒是很可能出現大額并購。OpenAI、Google、Anthropic、微軟、Meta這類公司都需要更強推理和驗證能力。對它們來說，幾十億美元收購一個頂級形式化推理團隊，不是離譜劇本。
原因很簡單。大模型公司都在往agent、coding、科研、企業自動化走。模型越能行動，越需要驗證。誰能把“模型輸出”變成“可檢查輸出”，誰就能在高價值場景里多賣一層信任。
所以Axiom、Harmonic這類公司，未必一定要先證明世界級數學難題，才有商業價值。只要它們證明自己能穩定生成可驗證代碼、可驗證推理、可驗證agent約束，就已經足夠讓大廠動心。
但并購不是技術成功的證明。它只說明大廠相信這條能力不能缺席。
另一個可能發生的局面，是生態分化。閉源公司做大模型和高端客戶，開源社區繼續建設LEAN、mathlib、LeanDojo、autoformalization工具。最后真正推動行業的，可能會是閉源模型、開源庫、數學家社區和企業驗證需求一起往前推。
所以未來三年，我會把預期放在三個層級：基礎設施一定會變厚，數學家日常工具會變好，高風險軟件驗證會開始試水。至于AI獨立成為研究級數學家，時間表還要往后放。
七、數學是 AI 的照妖鏡
7.1 數學的規則比藝術硬得多
回到開頭的Axiom故事，一個資深數論學家離開大學，加入一家年輕AI數學公司。這件事真正有意思的地方，不只是“老教授去了創業公司”，也不只是“2億美元融資”。它說明AI終于走到一個很難糊弄的場景里。
過去幾年，AI在藝術、寫作、圖片、視頻上給人的沖擊很大。但這些領域有一個共同特點：標準比較軟。你說這張圖好，我可以說它不夠高級；你說一段文案普通，我可以說它適合轉化；你說一段視頻怪，我可以說這是風格。
數學不吃這一套。
一個證明要么成立，要么不成立。一個LEAN證明通過了，就是通過了。沒通過，再像論文也沒有用。數學不給模型留“語氣很自信”“看起來很合理”“大概差不多”的空間。
這就是AI證明數學最迷人的地方。它不靠情緒，不靠風格，不靠“像不像”。它逼AI面對一個硬問題：你到底會不會推理？
7.2 數學家不會被一鍵替代
所以我不認為AI三年內會變成高斯、歐拉，也不認為數學家會被一鍵替代。
數學家的工作并不只是把一段證明從A推到B。真正難的地方，經常在證明之前：提出好問題，選擇好定義，判斷一個方向有沒有價值，決定該在哪個理論框架里看這個問題。很多時候，一個定義選錯了，后面證明再努力也會很難走。
AI現在更像一個很強的加速器。它可以幫你查mathlib，補lemma，驗證邊界條件，找反例，把一個證明草稿改成更嚴謹的形式。它尤其擅長吃掉那些枯燥、細碎、可驗證、需要大量試錯的部分。
這已經足夠大了。
如果過去一個數學家要花幾周把一個證明形式化，以后可能只需要幾小時或幾天。如果過去一個研究生要反復查庫、試tactic、補小引理，以后AI可以承擔大部分機械勞動。數學家的時間會更多地花在上游：問題、結構、定義、路線和解釋。
換句話說，數學家不會立刻消失，但數學家的工作流會變。越靠近“機械化證明勞動”的部分，越容易被AI吃掉；越靠近“提出什么問題、為什么值得做、用什么語言看它”的部分，越仍然需要人。
7.3 AI 終于遇到不能糊弄的考試
從Logic Theorist到AlphaProof，從希爾伯特的形式化夢想，到今天的LEAN和mathlib，AI繞了一大圈又回到原點。區別在于，這一次它不再只拿著手寫規則和小搜索樹，而是帶著神經網絡、強化學習、海量數據和真正可驗證的數學庫。
這條路最后能走多遠，現在沒人知道。黎曼猜想可能還很遠，研究級數學也不會被一夜之間自動化。可至少有一件事已經發生：AI終于開始接受一種它無法靠話術混過去的考試。
這個考試的結果，會反過來影響很多領域。
如果AI能在數學里學會“可驗證推理”，它就不只是在數學里有用。代碼驗證、科學推理、agent安全、金融風控、機器人控制，都需要類似能力。模型不能只給一個看起來合理的答案，還要能給出可以檢查的理由。
這也是為什么VC愿意給Axiom、Harmonic這種公司高估值。資本當然會講故事，也會制造泡沫。但泡沫背后有一個真實問題：當AI開始寫代碼、做決策、操作系統，人類需要某種硬驗證機制。數學證明是目前最硬的一種。
所以這篇文章的問題，不能只理解成“AI能不能發現新定理”。更準確地說，它在問：AI能不能從生成漂亮答案，走向生成可信答案？
如果答案是能，那數學只是第一塊試金石。如果答案是不能，那數學會成為AI能力邊界最誠實的照妖鏡。
作者其它文章
? 手把手教你分析：你會被AI取代嗎?
? 一篇文章講清大語言模型發展史
? 氣吞萬里如虎：回顧十九世紀的數學英豪們
? Vibe Reading：AI 時代讀書的系統化方法
? 長篇分析：Manus 案折射出的中國 AI 創業生態
? 別再被 AI 新詞繞暈了：Prompt、Context、Agent 背后的工程主線
? 兩萬字科普：AI 為什么會編程——原理、歷史與未來
? 兄弟們，真·Vibe Writing 時代到來了
? 全網最詳細的AI學習路線圖
? 每個人都應該使用的三個最有用的 Claude Skill
? SpaceX 立志傳（一）：賭上全部的最后一次發射
? 估值290億美元的套殼公司，正在被自己的房東殺死
? 黃仁勛和主持人吵紅了臉：芯片封鎖中國，美國到底能不能打贏？
? AI將如何顛覆教育，普通人又應該如何搶奪教育新的生態位
? 學物理的八方英雄們，物理學已死，請轉行搞AI
? 不會編程、沒有融資、沒有員工，他怎么一個人做到年入2000萬
? 兄弟們想清楚：究竟是你為X打工，還是X為你打工？
? 一人公司盈利四億美元：是騙子，還是可復制的紅利？
? 2026第一季度大裁員，AI是背鍋俠嗎？
? 重返星辰大海：這次繞月飛行有意義嗎？
? 張雪峰在美國為什么無法成功
? 2026 企業尸檢報告：不用AI，你的公司能活過今年嗎？
? 兄弟們，我創業失敗了，人生完整了
本文參考文獻
? Logic Theorist - Wikipedia
? LEAN Language Reference: History - LEAN官方Reference
? The LEAN Theorem Prover - Microsoft Research
? LEAN 4 Theorem Prover and Programming Language - Microsoft Research
? Mathlib: A Foundation for Formal Mathematics Research and Verification - LEAN官方Mathlib介紹
? AI achieves silver-medal standard solving International Mathematical Olympiad problems - Google DeepMind
? Harmonic About - Harmonic
? Aristotle: IMO-level Automated Theorem Proving - Harmonic
? Harmonic's IMO 2025 Results - GitHub
? Announcing Our Series C Funding - Harmonic
? AI Will Write All the Code. Mathematics Will Prove It Works. - Menlo Ventures
? Axiom Math Funding Round - Gaebler / VentureDeal
? Axiom - Axiom Math
? Ken Ono - University of Virginia
? The Math Legend Who Just Left Academia-for an AI Startup Run by a 24-Year-Old - Wall Street Journal
? AI For Math Fund Announces $18 Million In Grants - Renaissance Philanthropy
? AI for Math Fund - Renaissance Philanthropy
? Renaissance Philanthropy and XTX Markets Launch New $9 million AI for Math Fund - Renaissance Philanthropy
? LeanDojo: Theorem Proving with Retrieval-Augmented Language Models - NeurIPS 2023
? LeanDojo-v2: AI-Assisted Theorem Proving in LEAN - LeanDojo
? Is Math the Next AI Frontier? A Conversation with Terence Tao - Renaissance Philanthropy
? Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark - Harmonic
? Axiom LEAN Engine - Axiom Math
? The job description is changing: mathematician Terence Tao on the rise of AI - Nature
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
