2025年底，數(shù)學(xué)圈出了一個(gè)很有傳播性的故事。

數(shù)論學(xué)家Ken Ono離開(kāi)弗吉尼亞大學(xué)，加入硅谷AI初創(chuàng)公司Axiom Math。Ono做過(guò)美國(guó)數(shù)學(xué)會(huì)副主席，長(zhǎng)期研究拉馬努金和數(shù)論。按傳統(tǒng)路徑，他本來(lái)應(yīng)該繼續(xù)待在大學(xué)、研究所和講臺(tái)上。

Axiom Math由Carina Hong創(chuàng)辦。Hong當(dāng)時(shí)24歲，MIT數(shù)學(xué)和物理本科出身，后來(lái)進(jìn)入斯坦福讀博，又離開(kāi)學(xué)校創(chuàng)業(yè)。她想做一個(gè)AI數(shù)學(xué)家：能解決數(shù)學(xué)難題，能生成證明，也能檢查自己的推理是否正確。

這也是這個(gè)故事最抓人的地方：一位資深數(shù)學(xué)家，加入了一位年輕創(chuàng)業(yè)者剛剛成立的AI數(shù)學(xué)公司。放在幾年前，這樣的組合很難想象。

Axiom的大目標(biāo)，已經(jīng)越過(guò)了讓模型算題、寫答案這一步。它要讓AI學(xué)會(huì)做可靠的數(shù)學(xué)證明，把證明寫進(jìn)形式化系統(tǒng)里，讓機(jī)器能檢查每一步到底成立不成立。

幾個(gè)月后，資本市場(chǎng)也投了票。2026年3月，Axiom拿到2億美元A輪融資，估值約16億美元。一個(gè)剛成立不久的AI數(shù)學(xué)公司，靠“數(shù)學(xué)證明”講出了獨(dú)角獸故事。

最近幾年，AI在語(yǔ)言和圖像、視頻上都有了重大的突破。但是在數(shù)學(xué)上，AI的表現(xiàn)如何呢？數(shù)學(xué)不像寫文案、畫(huà)圖、做視頻。一個(gè)證明要么對(duì)，要么錯(cuò)。錯(cuò)一步，后面再漂亮也沒(méi)用。數(shù)學(xué)給AI提供了一把很硬的尺子。

如果AI只能寫出“看起來(lái)像證明”的文字，那它離真正的數(shù)學(xué)還很遠(yuǎn)。只有當(dāng)它能在這把尺子下面站住，我們才有資格繼續(xù)追問(wèn)更大的問(wèn)題。

所以問(wèn)題來(lái)了：AI能不能發(fā)現(xiàn)新的數(shù)學(xué)定理？它是在做更快的計(jì)算器，還是已經(jīng)開(kāi)始碰到人類創(chuàng)造知識(shí)的邊界？

一、AI 一開(kāi)始就是從數(shù)學(xué)證明里長(zhǎng)出來(lái)的

1.1 第一個(gè) AI 程序就在證明定理

很多人以為AI是最近幾年才開(kāi)始碰數(shù)學(xué)，其實(shí)剛好反過(guò)來(lái)。AI這個(gè)學(xué)科最早的代表作品之一，干的就是數(shù)學(xué)證明。

故事要從1950年代的RAND公司講起。

那時(shí)候還沒(méi)有“人工智能”這個(gè)正式學(xué)科。有三個(gè)學(xué)者在RAND湊到了一起：Allen Newell研究組織和決策，Herbert Simon研究人怎樣在有限信息下做選擇，Cliff Shaw負(fù)責(zé)把這些想法寫成真正能跑的程序。

Newell和Simon關(guān)心的問(wèn)題很直接：人類解決問(wèn)題的時(shí)候，到底在做什么？如果一個(gè)人能一步步推理、排除、搜索、試錯(cuò)，那么機(jī)器能不能也這么做？

他們挑的第一個(gè)靶子，是羅素和懷特海的《數(shù)學(xué)原理》。三卷本的《數(shù)學(xué)原理》是20世紀(jì)數(shù)學(xué)基礎(chǔ)研究里最有名的著作之一，試圖把數(shù)學(xué)建立在形式邏輯之上。書(shū)里的命題寫得非常嚴(yán)格，對(duì)機(jī)器來(lái)說(shuō)正好合適：規(guī)則清楚，目標(biāo)明確，每一步能不能走下去都可以檢查。

1955年底到1956年初，Logic Theorist的雛形做出來(lái)了。最有意思的是，最早的版本并不是直接在電腦上跑出來(lái)的。Simon后來(lái)回憶，他們把程序步驟寫在卡片上，讓家人和研究生分別扮演程序里的不同部件，像一臺(tái)“人肉計(jì)算機(jī)”一樣模擬程序運(yùn)行。

這聽(tīng)起來(lái)很原始，但它抓住了AI最早的核心想法：智能可以被拆成符號(hào)、規(guī)則和搜索。

等Shaw把程序真正搬到RAND的計(jì)算機(jī)上之后，Logic Theorist開(kāi)始證明《數(shù)學(xué)原理》第二章里的定理。它最后證明了前52個(gè)定理中的38個(gè)。一個(gè)亮點(diǎn)是，有些證明比原書(shū)還短。

1956年夏天，Dartmouth會(huì)議召開(kāi)，“Artificial Intelligence”這個(gè)詞在那里被正式推上臺(tái)面。Newell和Simon帶著Logic Theorist去參會(huì)。別人還在討論機(jī)器智能應(yīng)該是什么樣子，他們已經(jīng)拿出了一個(gè)會(huì)證明定理的程序。

所以AI從誕生第一天起，目標(biāo)就不只是模仿人類輸出。它一開(kāi)始想做的，就是邏輯推理，就是數(shù)學(xué)證明，就是讓機(jī)器進(jìn)入人類最硬的智力活動(dòng)之一。

1.2 希爾伯特的夢(mèng)被打碎，但工具留下了

再往上追，故事會(huì)回到希爾伯特。

20世紀(jì)初，數(shù)學(xué)家已經(jīng)擁有了微積分、集合論、非歐幾何、抽象代數(shù)，工具越來(lái)越強(qiáng)，地基卻越來(lái)越讓人不安。集合論里出現(xiàn)了悖論，幾何不再只有歐幾里得一種，分析學(xué)也剛剛經(jīng)歷嚴(yán)格化。數(shù)學(xué)家突然意識(shí)到：我們每天都在證明定理，但“證明”本身到底有多可靠？

希爾伯特的回答很硬。他希望把整個(gè)數(shù)學(xué)變成一套可以機(jī)械檢查的符號(hào)系統(tǒng)。所有概念先清楚定義，所有推理都按規(guī)則展開(kāi)，只要給出一個(gè)命題，原則上就能判斷它是真的、假的，還是能不能從公理里推出來(lái)。

這就是后來(lái)所謂的希爾伯特綱領(lǐng)。它有兩個(gè)核心愿望：第一，數(shù)學(xué)不能自相矛盾；第二，數(shù)學(xué)證明應(yīng)該能被有限、明確、可檢查的規(guī)則管住。換句話說(shuō)，數(shù)學(xué)不應(yīng)該只靠大師的直覺(jué)和讀者的信任，它應(yīng)該像一臺(tái)嚴(yán)密的機(jī)器。

這個(gè)夢(mèng)想非常誘人。它等于給數(shù)學(xué)找一張最終安全證書(shū)：只要公理系統(tǒng)是安全的，所有在里面推出的定理就都是安全的。羅素和懷特海寫《數(shù)學(xué)原理》，也可以放在這條大線里理解。

然后，1931年，哥德?tīng)杹?lái)了。

哥德?tīng)柌煌陚涠ɡ戆严柌刈顦?lè)觀的部分打碎了。他證明，在任何足夠強(qiáng)、足夠一致的形式系統(tǒng)里，總會(huì)存在一些真命題，無(wú)法在這個(gè)系統(tǒng)內(nèi)部被證明。更麻煩的是，這個(gè)系統(tǒng)也無(wú)法用自己的力量證明自己的一致性。

這句話聽(tīng)起來(lái)抽象，意思卻很重：數(shù)學(xué)不可能被完全壓成一臺(tái)萬(wàn)能判定機(jī)。你不能指望有一套終極規(guī)則，把所有數(shù)學(xué)命題都自動(dòng)判定完。

但希爾伯特的計(jì)劃并沒(méi)有完全白費(fèi)。

哥德?tīng)柎蛩榈氖恰叭詣?dòng)解決一切”的終極幻想，不是形式化本身。恰恰相反，形式邏輯、證明論、可計(jì)算性理論、類型論、自動(dòng)定理證明，后來(lái)都從這條線長(zhǎng)出來(lái)。它們承認(rèn)數(shù)學(xué)不可能被徹底機(jī)械化，但仍然努力把能機(jī)械化的部分盡量機(jī)械化。

AI的早期幾十年，尤其是所謂GOFAI，也就是Good Old-Fashioned AI，本質(zhì)上大量依賴符號(hào)、規(guī)則、搜索和邏輯。Logic Theorist能出現(xiàn)，背后就有這條形式化傳統(tǒng)。今天的工具LEAN、Coq、Isabelle，也是在這條路上繼續(xù)往前走。

1.3 從神經(jīng)網(wǎng)絡(luò)繞了一圈回到原點(diǎn)

按照1950年代那批人的想法，AI本來(lái)應(yīng)該沿著邏輯和證明一路往前走。機(jī)器會(huì)推理，會(huì)搜索，會(huì)證明定理，再往前一步，也許就能理解自然語(yǔ)言、規(guī)劃行動(dòng)、解決科學(xué)問(wèn)題。

現(xiàn)實(shí)沒(méi)有這么順。符號(hào)AI很快撞到墻。手寫規(guī)則太脆，真實(shí)世界太亂，常識(shí)太多，例外也太多。一個(gè)小小的場(chǎng)景變化，就可能讓精心寫好的規(guī)則失效。到后來(lái)，符號(hào)AI給人的感覺(jué)越來(lái)越像一座漂亮但難維護(hù)的宮殿：邏輯上很干凈，走出實(shí)驗(yàn)室就漏風(fēng)。

然后神經(jīng)網(wǎng)絡(luò)起來(lái)了。

它走的是另一條路：少寫規(guī)則，多喂數(shù)據(jù)。圖像識(shí)別、語(yǔ)音識(shí)別、機(jī)器翻譯、自然語(yǔ)言生成，都是這條路上打出來(lái)的勝仗。以前AI研究者想教機(jī)器“貓是什么”，現(xiàn)在直接給它看幾千萬(wàn)張圖。以前想手寫語(yǔ)言規(guī)則，現(xiàn)在讓模型從海量文本里自己學(xué)。

這條路線太成功了，以至于很多人開(kāi)始相信：智能不需要顯式規(guī)則，只要模型夠大、數(shù)據(jù)夠多、訓(xùn)練夠狠，它就能自己長(zhǎng)出來(lái)。符號(hào)、邏輯、證明這些老詞，突然顯得又慢又土。

但數(shù)學(xué)證明沒(méi)有那么容易被繞開(kāi)。

你可以用神經(jīng)網(wǎng)絡(luò)寫一段“很像證明”的文字，但數(shù)學(xué)不會(huì)因?yàn)樗窬头判?。證明需要每一步都成立，需要變量、定義、定理、前提條件全部對(duì)上。這里的麻煩，恰好是符號(hào)系統(tǒng)最擅長(zhǎng)處理的東西。

所以現(xiàn)在劇情又繞回來(lái)了，而且不是一個(gè)實(shí)驗(yàn)室在自嗨。

Google DeepMind在做AlphaProof，把AlphaGo、AlphaZero那套神經(jīng)網(wǎng)絡(luò)加搜索的思路，搬進(jìn)形式化數(shù)學(xué)證明。Harmonic在做Aristotle，目標(biāo)是讓模型直接產(chǎn)出能被LEAN檢查的證明。Axiom Math押的是另一條更商業(yè)化的線：如果未來(lái)AI會(huì)寫大量代碼和科學(xué)推理，那么數(shù)學(xué)證明就可以變成驗(yàn)證這些輸出是否可靠的工具。

這些項(xiàng)目的技術(shù)細(xì)節(jié)各不相同，但底層結(jié)構(gòu)很像：用神經(jīng)網(wǎng)絡(luò)猜路，用強(qiáng)化學(xué)習(xí)和搜索擴(kuò)大嘗試范圍，再用形式化系統(tǒng)驗(yàn)算。機(jī)器先提出可能的證明路徑，LEAN這類系統(tǒng)負(fù)責(zé)一行行檢查。猜錯(cuò)了就退回去，猜對(duì)了才算真正往前走。

繞了70年，AI又回到Logic Theorist的出發(fā)點(diǎn)。區(qū)別在于，這一次它手里多了算力、數(shù)據(jù)、強(qiáng)化學(xué)習(xí)，還有LEAN這樣的形式化地基。

二、LEAN: 這場(chǎng)游戲的地基

2.1 LEAN 是檢查證明的機(jī)器

要理解AI證明數(shù)學(xué)，先要理解LEAN。

LEAN本身是一個(gè)定理證明器，也可以理解成一種極其嚴(yán)格的數(shù)學(xué)編程語(yǔ)言。它不負(fù)責(zé)和你聊天，也不負(fù)責(zé)替你“發(fā)揮”。你在LEAN里寫的是定義、命題和證明。

普通數(shù)學(xué)證明寫在紙上，靠同行閱讀、審稿和學(xué)術(shù)共同體來(lái)判斷對(duì)錯(cuò)。人類寫證明時(shí)，經(jīng)常會(huì)說(shuō)“顯然”“由標(biāo)準(zhǔn)結(jié)論可知”“不難推出”。這些話在論文里可以成立，因?yàn)樽x者默認(rèn)作者和審稿人知道中間省略了什么。

LEAN不接受這種省略。

你在LEAN里寫一步，它就檢查一步。變量類型對(duì)不對(duì)，前提條件有沒(méi)有給齊，調(diào)用的定理能不能用，目標(biāo)有沒(méi)有真的被證明完，它都會(huì)檢查。只要LEAN接受，這個(gè)證明就在它的公理系統(tǒng)和庫(kù)依賴下成立。它不看文風(fēng)，不看氣勢(shì)，也不看作者名氣。

所以你可以把LEAN想成數(shù)學(xué)世界里的編譯器。

寫程序時(shí)，編譯器不關(guān)心你覺(jué)得代碼“應(yīng)該能跑”。它只看語(yǔ)法、類型和規(guī)則。LEAN也是這樣。你說(shuō)“顯然可得”沒(méi)有用，除非你把“顯然”的每一步都寫清楚，或者調(diào)用庫(kù)里已經(jīng)證明過(guò)的定理。

這就是LEAN和ChatGPT式數(shù)學(xué)輸出的根本差別。ChatGPT可以寫出一段很像證明的文字，讀起來(lái)順，但中間可能有坑。LEAN里的證明要么通過(guò)檢查，要么報(bào)錯(cuò)。它把“像不像證明”變成了“是不是證明”。

2.2 Leonardo de Moura 為什么要做 LEAN

LEAN的核心人物是Leonardo de Moura。他是微軟研究院的研究員，長(zhǎng)期做自動(dòng)推理和形式化驗(yàn)證。

他更早的代表作之一是Z3，微軟研究院開(kāi)發(fā)的SMT求解器。SMT求解器可以理解成一種自動(dòng)邏輯工具，擅長(zhǎng)在很多約束條件里判斷是否存在解，廣泛用在程序驗(yàn)證、硬件驗(yàn)證和軟件工程里。

但自動(dòng)工具有一個(gè)問(wèn)題：它們很強(qiáng)，也很黑箱。你把問(wèn)題丟進(jìn)去，它給你答案；可是一旦問(wèn)題變得非常抽象、非常數(shù)學(xué)化，人還是需要參與構(gòu)造證明。傳統(tǒng)交互式證明器正好相反，人可以一步步寫證明，但自動(dòng)化又經(jīng)常不夠順手。

LEAN想把這兩邊接起來(lái)。

2013年，de Moura在微軟研究院?jiǎn)?dòng)LEAN項(xiàng)目。官方Reference里寫得很清楚：LEAN的目標(biāo)，是把一個(gè)很小、可以獨(dú)立實(shí)現(xiàn)的可信邏輯內(nèi)核，和SMT求解器這類自動(dòng)化工具的便利性結(jié)合起來(lái)，同時(shí)能擴(kuò)展到大問(wèn)題。

這句話翻成白話就是：底層要足夠小，才能讓人相信；上層要足夠好用，數(shù)學(xué)家和程序員才愿意真的寫東西。

2015年，de Moura、Soonho Kong、Jeremy Avigad、Floris van Doorn和Jakob von Raumer在CADE會(huì)議上發(fā)表了LEAN的系統(tǒng)論文。那篇論文把LEAN定義為一個(gè)開(kāi)源定理證明器，使用基于依賴類型論的小型可信內(nèi)核，目標(biāo)是連接交互式證明和自動(dòng)證明。

這也是LEAN后來(lái)能長(zhǎng)大的關(guān)鍵。它一開(kāi)始就沒(méi)有只想做一個(gè)學(xué)術(shù)玩具，而是想做一個(gè)平臺(tái)：可以寫數(shù)學(xué)，可以做軟件驗(yàn)證，可以做教育，也可以讓自動(dòng)化工具嵌進(jìn)來(lái)。

2.3 從 LEAN 3 到 LEAN 4：從證明器變成語(yǔ)言

LEAN最早的版本更像研究原型。

官方歷史里寫到，LEAN 0.1在2014年6月發(fā)布。早期版本主要以C++庫(kù)的形式存在，讓其他程序可以調(diào)用它來(lái)構(gòu)造可檢查的證明。后來(lái)，LEAN逐漸往傳統(tǒng)交互式證明器演化，先有Lua寫的tactic，再有專門的前端語(yǔ)法。

2017年1月，LEAN 3發(fā)布。對(duì)數(shù)學(xué)社區(qū)來(lái)說(shuō)，這是一個(gè)關(guān)鍵節(jié)點(diǎn)。LEAN 3足夠穩(wěn)定，也足夠可擴(kuò)展，數(shù)學(xué)家開(kāi)始認(rèn)真拿它干活。更重要的是，它支持很強(qiáng)的自擴(kuò)展能力：tactic、記號(hào)、頂層命令，都可以用LEAN自己定義。

這聽(tīng)起來(lái)像語(yǔ)言設(shè)計(jì)細(xì)節(jié)，其實(shí)影響很大。數(shù)學(xué)不是一套固定格式。代數(shù)有代數(shù)的寫法，拓?fù)溆型負(fù)涞膶懛?，范疇論有范疇論的寫法。如果一個(gè)證明器不能讓社區(qū)自己擴(kuò)展語(yǔ)言和工具，它很難承載現(xiàn)代數(shù)學(xué)的復(fù)雜表達(dá)。

LEAN 3的成功也帶來(lái)一個(gè)問(wèn)題：系統(tǒng)本身主要還是C++實(shí)現(xiàn)，擴(kuò)展起來(lái)有成本。于是LEAN 4開(kāi)始重寫。

2018年，LEAN 4開(kāi)發(fā)啟動(dòng)。2023年9月，LEAN 4.0正式發(fā)布。它是新版證明器，也是一門更完整的函數(shù)式編程語(yǔ)言。官方Reference里說(shuō)，到了LEAN 4，大約90%的LEAN實(shí)現(xiàn)代碼本身用LEAN寫成，也就是所謂self-hosted。

這里很容易誤解。LEAN 4不是一個(gè)“把人類證明自動(dòng)翻譯成機(jī)器語(yǔ)言”的轉(zhuǎn)換器。它更像一個(gè)數(shù)學(xué)證明的編程環(huán)境：你在里面定義對(duì)象，寫下命題，再把證明寫成一行行代碼。LEAN 4負(fù)責(zé)檢查這些證明代碼是否真的成立。

把自然語(yǔ)言證明翻譯成LEAN代碼，是另一個(gè)問(wèn)題，叫autoformalization。比如論文里寫“顯然，由緊性可知存在有限子覆蓋”，翻成LEAN時(shí)，你要說(shuō)明空間類型、緊性的定義、開(kāi)覆蓋怎么表示、調(diào)用哪個(gè)已有定理。翻譯完以后，LEAN 4還要繼續(xù)檢查它。

這一步很重要。它意味著LEAN不再只是“檢查數(shù)學(xué)證明的工具”，也變成了“寫工具的工具”。用戶可以更方便地做自定義語(yǔ)法、自動(dòng)化tactic、領(lǐng)域?qū)Ｓ霉ぞ?。?duì)AI證明數(shù)學(xué)來(lái)說(shuō)，這一點(diǎn)尤其關(guān)鍵，因?yàn)锳I不只需要一個(gè)判卷老師，還需要一個(gè)可以嵌入搜索、生成、反饋和自動(dòng)化的環(huán)境。

2.4 mathlib 是 AI 數(shù)學(xué)的工具箱

真正讓LEAN變成AI數(shù)學(xué)基礎(chǔ)設(shè)施的，是mathlib。

mathlib是LEAN社區(qū)維護(hù)的數(shù)學(xué)庫(kù)。它的目標(biāo)很樸素，也很瘋狂：把盡可能多的現(xiàn)代數(shù)學(xué)，翻譯成機(jī)器可檢查的定義、定理和證明。

一個(gè)證明器本身再漂亮，如果沒(méi)有庫(kù)，也很難做事。就像你寫程序，不會(huì)每次都從零實(shí)現(xiàn)數(shù)組、哈希表、網(wǎng)絡(luò)協(xié)議和文件系統(tǒng)。數(shù)學(xué)也是一樣。你要證明一個(gè)數(shù)論命題，可能要用群、環(huán)、域、拓?fù)洹⒎治觥⒔M合、序理論、范疇論里的很多舊結(jié)論。沒(méi)有庫(kù)，每一步都要從公理開(kāi)始，根本走不遠(yuǎn)。

mathlib解決的就是這個(gè)問(wèn)題。

它把代數(shù)、分析、拓?fù)?、?shù)論、組合、范疇論等大量數(shù)學(xué)內(nèi)容，一條條翻譯成LEAN可以檢查的形式。這個(gè)工作非常慢，也非常苦。很多時(shí)候，一個(gè)人類論文里一句“由標(biāo)準(zhǔn)結(jié)論可知”，在LEAN里可能要展開(kāi)成幾十行甚至幾百行代碼。

LEAN 3時(shí)代，mathlib已經(jīng)積累到超過(guò)100萬(wàn)行形式化數(shù)學(xué)。2023年，社區(qū)又把mathlib遷移到LEAN 4。官方Reference提到，遷移完成后，mathlib繼續(xù)增長(zhǎng)到超過(guò)150萬(wàn)行，而且LEAN 4檢查更大的庫(kù)，速度反而比LEAN 3檢查較小的庫(kù)更快。

這不是一個(gè)小工程。它更像把數(shù)學(xué)世界一塊塊搬進(jìn)機(jī)器能讀的城市里。每搬進(jìn)去一個(gè)定義、一個(gè)引理、一個(gè)定理，后面的人和AI就少走一步路。

所以AI數(shù)學(xué)這輪變化，底層并不只是“模型突然變聰明”。它是兩件事疊在一起：形式化社區(qū)先花多年修路，神經(jīng)網(wǎng)絡(luò)再用搜索和訓(xùn)練把這條路跑得更快。

2.5 為什么 AI 最終會(huì)盯上 LEAN

現(xiàn)在再回頭看，AI盯上LEAN并不奇怪。

大語(yǔ)言模型擅長(zhǎng)生成候選答案，但它最大的問(wèn)題是不可驗(yàn)證。它可以寫出一段語(yǔ)氣很像數(shù)學(xué)家的證明，也可以一本正經(jīng)寫錯(cuò)。自然語(yǔ)言證明里有太多省略，普通讀者甚至很難看出錯(cuò)在哪里。

LEAN給AI提供了一個(gè)罕見(jiàn)的訓(xùn)練環(huán)境。

模型每寫一步證明，LEAN都能給出干凈反饋：通過(guò)，或者不通過(guò)。這個(gè)反饋非常適合搜索和強(qiáng)化學(xué)習(xí)。模型可以先猜一個(gè)證明步驟，LEAN檢查；失敗就換路，成功就繼續(xù)。成功路徑還能變成新的訓(xùn)練數(shù)據(jù)。

這就是為什么DeepMind、Harmonic、Axiom這些玩家都繞不開(kāi)LEAN和mathlib。DeepMind需要一個(gè)可驗(yàn)證的競(jìng)賽數(shù)學(xué)環(huán)境，Harmonic需要證明文件真正通過(guò)檢查，Axiom需要把數(shù)學(xué)證明變成代碼和科學(xué)推理的可信底座。

換句話說(shuō)，LEAN不是AI數(shù)學(xué)故事里的配角。它更像這場(chǎng)游戲的地基。沒(méi)有它，模型只能生成“看起來(lái)像證明”的文字；有了它，AI才有機(jī)會(huì)把猜想、搜索和驗(yàn)證連成一個(gè)閉環(huán)。

三、現(xiàn)在的玩家已經(jīng)不只是實(shí)驗(yàn)室

3.1 DeepMind 把 IMO 變成公開(kāi)靶場(chǎng)

2024年7月，Google DeepMind把這個(gè)方向推到大眾視野里。它沒(méi)有先去宣布“AI要解決黎曼猜想”，而是選了一個(gè)所有人都看得懂的靶場(chǎng)：國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽，IMO。

IMO有兩個(gè)好處。第一，題目足夠難，全世界最強(qiáng)中學(xué)生都在這里競(jìng)爭(zhēng)。第二，規(guī)則很清楚，滿分42分，6道題，每道7分，最后可以直接和人類選手比較。對(duì)AI來(lái)說(shuō)，這是一個(gè)天然的公開(kāi)benchmark。

DeepMind發(fā)布的系統(tǒng)叫AlphaProof和AlphaGeometry 2。前者主攻代數(shù)、數(shù)論這類可以走形式化證明路線的問(wèn)題；后者主攻幾何。兩個(gè)系統(tǒng)合起來(lái)，在2024年IMO上解出6道題中的4道，總分28分，達(dá)到銀牌上沿。那一年金牌線是29分，它離金牌只差1分。

這件事真正刺激人的地方，不只是“AI會(huì)做奧數(shù)題”。更關(guān)鍵的是，AlphaProof走的是形式化證明路線。它把自然語(yǔ)言問(wèn)題轉(zhuǎn)成形式化表達(dá)，再用強(qiáng)化學(xué)習(xí)和搜索去找證明，最后讓證明系統(tǒng)檢查。DeepMind等于把AlphaGo、AlphaZero那套“神經(jīng)網(wǎng)絡(luò)加搜索加強(qiáng)化學(xué)習(xí)”的結(jié)構(gòu)，搬到了數(shù)學(xué)證明里。

這和普通模型寫一段漂亮證明完全不同。普通模型可以胡說(shuō)，AlphaProof要讓機(jī)器驗(yàn)算。它做出來(lái)的東西，至少要在形式系統(tǒng)里站得住。

但這里也要潑一盆冷水。IMO金牌級(jí)不等于研究級(jí)數(shù)學(xué)家。

競(jìng)賽題是人為設(shè)計(jì)的封閉問(wèn)題，條件清楚，目標(biāo)明確，答案一定存在。研究級(jí)數(shù)學(xué)經(jīng)常連正確問(wèn)題是什么都不清楚，更不用說(shuō)把它翻譯成LEAN里的精確定義。真正的數(shù)學(xué)研究還需要選題、定義、品味、背景判斷和長(zhǎng)期的理論積累。

3.2 Harmonic 和 Axiom 把數(shù)學(xué)證明做成公司

DeepMind的意義，是證明這條路能打公開(kāi)比賽。Harmonic和Axiom的意義，是把這條路做成公司。

先看Harmonic。

Harmonic由Tudor Achim和Robinhood聯(lián)合創(chuàng)始人Vlad Tenev創(chuàng)辦。它對(duì)外講的詞很大，叫Mathematical Superintelligence，數(shù)學(xué)超級(jí)智能。這個(gè)詞當(dāng)然有營(yíng)銷成分，但它背后的問(wèn)題很具體：如果AI經(jīng)常幻覺(jué)，能不能用數(shù)學(xué)證明把它按?。?/p>

Harmonic的核心產(chǎn)品叫Aristotle。到了2025年，Aristotle在IMO方向又往前走了一步。Harmonic官方披露，Aristotle在2025年IMO上達(dá)到金牌級(jí)表現(xiàn)，形式化解決了6道題中的5道，并開(kāi)源了部分LEAN證明文件。它的技術(shù)報(bào)告里也明確說(shuō)，只有系統(tǒng)產(chǎn)出完整的LEAN 4證明，而且沒(méi)有sorryAx這類不可靠占位，才算真正解決。

這個(gè)標(biāo)準(zhǔn)很硬。很多系統(tǒng)做數(shù)學(xué)題，是寫出一個(gè)看起來(lái)合理的解答。Aristotle要交的是可以被LEAN檢查的證明文件。一個(gè)占位符、一個(gè)沒(méi)有補(bǔ)完的證明洞，都不能算數(shù)。

資本也迅速跟上。Harmonic 2025年11月宣布完成1.2億美元Series C，估值14.5億美元。它已經(jīng)是一家圍繞“可驗(yàn)證數(shù)學(xué)推理”融資、招人、做API的AI公司。

另一個(gè)明星公司是Axiom Math。Axiom由Carina Hong創(chuàng)辦，2026年3月，Menlo Ventures宣布領(lǐng)投它2億美元A輪，投后估值16億美元。

Axiom的招人故事也很有傳播性。Ken Ono，這位數(shù)論領(lǐng)域的知名數(shù)學(xué)家，離開(kāi)弗吉尼亞大學(xué)的學(xué)術(shù)崗位加入Axiom，擔(dān)任founding mathematician。一位資深數(shù)學(xué)家加入年輕創(chuàng)業(yè)者創(chuàng)辦的AI數(shù)學(xué)公司，本身就足夠抓眼球。

那Axiom到底做什么？

它的目標(biāo)不是做一個(gè)“會(huì)聊天的數(shù)學(xué)模型”，也不只是幫數(shù)學(xué)家證明幾個(gè)漂亮定理。Axiom押的是Verified AI，也就是可驗(yàn)證的AI。它要讓模型生成的東西，最后能被形式化證明檢查。

最直接的場(chǎng)景是代碼。未來(lái)AI會(huì)寫大量代碼，但“能跑”“通過(guò)測(cè)試”“看起來(lái)沒(méi)問(wèn)題”都不等于安全。金融交易、加密協(xié)議、自動(dòng)駕駛、醫(yī)療系統(tǒng)、AI基礎(chǔ)設(shè)施里的代碼，錯(cuò)一次代價(jià)可能很高。Axiom想做的，是讓AI寫出來(lái)的關(guān)鍵代碼和關(guān)鍵推理，能夠被數(shù)學(xué)證明驗(yàn)證：這個(gè)函數(shù)對(duì)所有輸入都返回正確結(jié)果，這段邏輯不會(huì)破壞數(shù)據(jù)，這個(gè)系統(tǒng)不會(huì)引入某類安全漏洞。

所以Axiom的商業(yè)敘事不是“數(shù)學(xué)家失業(yè)”。它更像是在給AI生成代碼和AI推理加一層可信度。AI負(fù)責(zé)生產(chǎn)，Axiom負(fù)責(zé)證明這些輸出真的符合規(guī)格。

Axiom自己也在做工具層。它公開(kāi)的AXLE，也就是Axiom LEAN Engine，提供的是探索、驗(yàn)證、操作數(shù)學(xué)證明的交互式工具。你可以把它理解成Axiom內(nèi)部訓(xùn)練和驗(yàn)證系統(tǒng)的一部分：模型生成證明，AXLE/LEAN這類工具負(fù)責(zé)檢查、提取定理、操作證明對(duì)象。

所以Harmonic和Axiom看起來(lái)都在做AI數(shù)學(xué)，側(cè)重點(diǎn)并不一樣。Harmonic更像從數(shù)學(xué)推理模型往外擴(kuò)，Axiom更像從可信AI和代碼驗(yàn)證往里打。它們共同說(shuō)明一件事：數(shù)學(xué)證明已經(jīng)從學(xué)術(shù)實(shí)驗(yàn)，變成了AI創(chuàng)業(yè)公司的核心敘事。

3.3 錢開(kāi)始流向基礎(chǔ)設(shè)施，但研究級(jí)數(shù)學(xué)還很遠(yuǎn)

與此同時(shí)，錢也開(kāi)始進(jìn)入基礎(chǔ)設(shè)施層。

這一點(diǎn)很重要。真正推動(dòng)AI數(shù)學(xué)的，不會(huì)只有幾家閉源公司。它還需要數(shù)據(jù)集、形式化庫(kù)、autoformalization工具、LEAN教學(xué)、現(xiàn)代定理形式化項(xiàng)目。換句話說(shuō)，它需要一整套公共基礎(chǔ)設(shè)施。

XTX Markets和Renaissance Philanthropy就是這一層的代表。AI for Math Fund最初由XTX Markets支持，后來(lái)擴(kuò)大到1800萬(wàn)美元，資助29個(gè)項(xiàng)目。2026年3月，Renaissance Philanthropy和XTX又宣布追加1350萬(wàn)美元，把總承諾提高到3150萬(wàn)美元。

這些錢投向的東西很具體：形式化數(shù)學(xué)數(shù)據(jù)集，autoformalization工具，LEAN教學(xué)，把現(xiàn)代數(shù)學(xué)定理搬進(jìn)形式化庫(kù)。比如有項(xiàng)目要把頂級(jí)數(shù)學(xué)期刊里的現(xiàn)代定理形式化出來(lái)，有項(xiàng)目要做本科生證明的自動(dòng)形式化和反饋工具。

這里還必須提一個(gè)開(kāi)源項(xiàng)目：LeanDojo。

LeanDojo由Caltech、NVIDIA、MIT等機(jī)構(gòu)的研究者在2023年推出，論文發(fā)表在NeurIPS 2023。它解決的是一個(gè)很工程、但很關(guān)鍵的問(wèn)題：機(jī)器學(xué)習(xí)模型怎么和LEAN交互？如果每個(gè)團(tuán)隊(duì)都自己寫一套抽取數(shù)據(jù)、運(yùn)行證明、記錄狀態(tài)、評(píng)測(cè)結(jié)果的工具，這個(gè)領(lǐng)域很難復(fù)現(xiàn)，也很難積累。

LeanDojo做了兩件底層工作。第一，它從LEAN和mathlib里抽取證明數(shù)據(jù)、proof state、tactic和premise信息，做成可以訓(xùn)練模型的數(shù)據(jù)。第二，它把LEAN變成一個(gè)類似gym的交互環(huán)境：模型可以看到當(dāng)前證明狀態(tài)，提交下一步tactic，LEAN返回成功、失敗或新的子目標(biāo)。

它還提出了ReProver，一個(gè)帶檢索的證明模型。這個(gè)思路很自然：證明一個(gè)定理時(shí)，模型不能只靠自己背下來(lái)的參數(shù)，它還要從龐大的數(shù)學(xué)庫(kù)里找可能用得上的舊定理。LeanDojo論文里構(gòu)造了接近10萬(wàn)個(gè)來(lái)自mathlib的定理和證明，用來(lái)訓(xùn)練和評(píng)測(cè)這種檢索增強(qiáng)的證明器。

所以LeanDojo的意義，不在于它自己是不是最強(qiáng)的數(shù)學(xué)AI。它更像一個(gè)開(kāi)放訓(xùn)練場(chǎng)，把“模型如何讀LEAN、如何和LEAN互動(dòng)、如何從mathlib里找工具”這件事標(biāo)準(zhǔn)化。后來(lái)的很多AI證明工作，都離不開(kāi)這種基礎(chǔ)設(shè)施。

陶哲軒（Terence Tao）也在這個(gè)基金的顧問(wèn)名單里，并多次公開(kāi)談到AI和LEAN對(duì)數(shù)學(xué)協(xié)作的潛力。他的態(tài)度很有代表性：AI短期內(nèi)不是按一下按鈕就吐出深定理的神機(jī)，更像一個(gè)能幫數(shù)學(xué)家查庫(kù)、補(bǔ)引理、找邊界、整理證明的協(xié)作工具。

這說(shuō)明AI數(shù)學(xué)已經(jīng)過(guò)了“幾個(gè)研究員做benchmark”的階段。大廠、創(chuàng)業(yè)公司、VC、交易公司、慈善基金、數(shù)學(xué)家，都開(kāi)始把它當(dāng)成一條可能改變科研和軟件工業(yè)的基礎(chǔ)路線。

四、AI 到底怎么證明一個(gè)定理

4.1 AI 負(fù)責(zé)猜，LEAN 負(fù)責(zé)判

AI證明數(shù)學(xué)的核心結(jié)構(gòu)，可以壓成一句話：AI猜，LEAN判。

想象你給系統(tǒng)一個(gè)命題：證明某個(gè)數(shù)論結(jié)論，或者證明某段代碼滿足某個(gè)規(guī)格。第一步是把目標(biāo)放進(jìn)LEAN這樣的形式化環(huán)境里，而不是先寫一段漂亮解釋。系統(tǒng)要知道對(duì)象是什么，變量是什么，前提是什么，最后要證明的目標(biāo)是什么。

然后模型開(kāi)始猜路。

它讀過(guò)大量數(shù)學(xué)材料和LEAN代碼，學(xué)過(guò)命題怎么寫、定義怎么展開(kāi)、證明套路怎么走、tactic怎么用。面對(duì)一個(gè)新目標(biāo)，它可能先生成一個(gè)證明步驟，也可能先拆出幾個(gè)中間引理。比如先證明一個(gè)更小的等式，再把這個(gè)等式接回原目標(biāo)。

LEAN做另一件事。它不負(fù)責(zé)靈感，不負(fù)責(zé)猜路，只負(fù)責(zé)驗(yàn)算。模型寫出一行LEAN證明，LEAN檢查這行是否成立。通過(guò)就進(jìn)入下一個(gè)狀態(tài)，不通過(guò)就報(bào)錯(cuò)。

這就像一個(gè)人負(fù)責(zé)想下一步棋，另一個(gè)裁判負(fù)責(zé)判斷這步棋合不合法。AI的價(jià)值在于提出候選路徑，LEAN的價(jià)值在于保證每一步?jīng)]有偷渡。

4.2 它和 ChatGPT 寫證明不是一回事

這和普通ChatGPT寫數(shù)學(xué)證明差別很大。

ChatGPT可以寫出一段非常像人類論文的證明。它會(huì)說(shuō)“由緊性可知”“顯然存在”“不難推出”，讀起來(lái)很順。但只要中間某個(gè)“顯然”其實(shí)不成立，整段文字就塌了。更麻煩的是，很多讀者看不出來(lái)它塌在哪里。

LEAN不吃這一套。你不能用語(yǔ)氣騙過(guò)它。一個(gè)變量類型不對(duì)，一個(gè)條件沒(méi)傳進(jìn)去，一個(gè)定理適用范圍不滿足，它都會(huì)報(bào)錯(cuò)。AI在LEAN里寫證明，等于每一步都要過(guò)安檢。

舉一個(gè)很小的例子。人類論文里寫“由緊性可知存在有限子覆蓋”，讀者大概能懂。但在LEAN里，這句話要變成一串明確操作：當(dāng)前空間是什么類型，緊性定義調(diào)用哪一個(gè)，開(kāi)覆蓋如何表示，有限子覆蓋是哪個(gè)對(duì)象，用哪個(gè)已有定理把它拿出來(lái)。

如果其中一個(gè)對(duì)象類型不對(duì)，LEAN就不會(huì)讓你往下走。它不會(huì)因?yàn)檫@句話“數(shù)學(xué)味很足”就放行。

所以普通模型寫證明，是在生成一段像證明的文本。AI加LEAN寫證明，是在生成一段會(huì)被機(jī)器逐步檢查的證明代碼。這兩件事差別很大。

4.3 檢索舊定理，生成下一步 tactic

真正的證明很少?gòu)牧汩_(kāi)始。

數(shù)學(xué)家做證明，也會(huì)先想：這個(gè)問(wèn)題像不像某個(gè)已知定理？有沒(méi)有可以調(diào)用的引理？這個(gè)結(jié)構(gòu)是不是應(yīng)該用緊性、完備性、歸納法、同構(gòu)、范疇論里的某個(gè)標(biāo)準(zhǔn)工具？

AI也要做類似的事。它不能只靠參數(shù)里“記住”的數(shù)學(xué)知識(shí)。mathlib太大了，定理太多了，很多時(shí)候關(guān)鍵不在于模型會(huì)不會(huì)寫下一行，而在于它能不能找到該用哪一個(gè)舊定理。

這就是LeanDojo和ReProver那類工作的意義。模型看到當(dāng)前proof state以后，先從mathlib里檢索可能有用的premise，再把這些候選定理和當(dāng)前目標(biāo)一起喂給模型，讓它生成下一步tactic。

Tactic可以理解成LEAN里的證明動(dòng)作。它可能是“用這個(gè)定理改寫目標(biāo)”，可能是“把目標(biāo)拆成兩個(gè)子目標(biāo)”，可能是“對(duì)自然數(shù)做歸納”，也可能是“把某個(gè)條件交給自動(dòng)化工具處理”。每走一步，LEAN都會(huì)返回新的proof state。

于是證明過(guò)程變成一棵搜索樹(shù)。一個(gè)目標(biāo)可以往很多方向走，有些方向馬上報(bào)錯(cuò)，有些方向走幾步才死，有些方向能把目標(biāo)拆小，最后一路走到所有子目標(biāo)都被解決。

4.4 強(qiáng)化學(xué)習(xí)吃到了干凈反饋

這個(gè)結(jié)構(gòu)特別適合強(qiáng)化學(xué)習(xí)。因?yàn)長(zhǎng)EAN給出的反饋非常干凈：通過(guò)，或者不通過(guò)。沒(méi)有“看起來(lái)還行”，沒(méi)有“老師給你5分辛苦分”。模型可以在LEAN環(huán)境里反復(fù)嘗試，把成功路徑當(dāng)成訓(xùn)練數(shù)據(jù)，把失敗路徑丟掉或修正。

這也是為什么DeepMind那批做過(guò)AlphaGo、AlphaZero的人會(huì)撲向數(shù)學(xué)證明。圍棋有一個(gè)規(guī)則明確的棋盤，走法對(duì)錯(cuò)和勝負(fù)可以被系統(tǒng)判定。形式化數(shù)學(xué)也有一個(gè)規(guī)則明確的符號(hào)世界，證明是否成立可以被LEAN判定。

但數(shù)學(xué)比圍棋麻煩得多。

圍棋棋盤有限，規(guī)則固定，目標(biāo)就是贏。數(shù)學(xué)里的“下一步該引入什么定義”“該證明哪個(gè)引理”“這個(gè)問(wèn)題應(yīng)該放進(jìn)哪個(gè)理論框架”，沒(méi)有那么清楚。證明空間大得離譜，很多時(shí)候連搜索方向都需要人類數(shù)學(xué)直覺(jué)。

所以現(xiàn)在的系統(tǒng)通常不會(huì)只靠模型一次生成完整證明。它更像是在一個(gè)形式化環(huán)境里反復(fù)試：生成若干候選tactic，LEAN檢查，保留能推進(jìn)的路徑，失敗的路徑回退。搜索算法負(fù)責(zé)在許多候選路徑之間分配計(jì)算資源，模型負(fù)責(zé)提出更可能有用的下一步。

一旦某條路徑最終通過(guò)，系統(tǒng)就得到一個(gè)干凈樣本：這條證明是真的。這個(gè)樣本可以繼續(xù)拿來(lái)訓(xùn)練模型。失敗路徑也有用，因?yàn)樗嬖V模型哪些操作不該在類似狀態(tài)下使用。

這就是AI證明數(shù)學(xué)吸引人的地方。它不像寫文章那樣很難判分，也不像很多科學(xué)實(shí)驗(yàn)?zāi)菢臃答伮?。形式化證明給了模型一個(gè)快速、明確、可重復(fù)的訓(xùn)練信號(hào)。

4.5 Autoformalization 是最硬的瓶頸

所以現(xiàn)在最難的瓶頸之一，是autoformalization。

這個(gè)詞指的是把人類自然語(yǔ)言寫的數(shù)學(xué)，自動(dòng)翻譯成LEAN里的形式化表達(dá)。它包括兩層：把命題翻譯成LEAN里的精確定義，也把證明翻譯成LEAN可以檢查的步驟。

它難在好幾層。

第一層是省略。比如論文里寫“令X為緊Hausdorff空間”，LEAN需要知道你調(diào)用的是哪個(gè)拓?fù)浣Y(jié)構(gòu)、哪些實(shí)例、哪些已有定理。論文里寫“由標(biāo)準(zhǔn)結(jié)論可知”，LEAN要知道這個(gè)標(biāo)準(zhǔn)結(jié)論到底是哪一個(gè)定理，前提條件是否滿足，變量如何對(duì)應(yīng)。

人類數(shù)學(xué)家默認(rèn)共享的大量背景，在機(jī)器眼里都要顯式寫出來(lái)。

第二層是概念選擇。同一個(gè)數(shù)學(xué)對(duì)象，可以用不同方式形式化。一個(gè)群作用、一個(gè)拓?fù)淇臻g、一個(gè)范疇里的對(duì)象，放進(jìn)LEAN時(shí)要選哪套定義？選錯(cuò)了，后面可能每一步都很難走。人類數(shù)學(xué)家會(huì)憑經(jīng)驗(yàn)選擇最順的語(yǔ)言，機(jī)器現(xiàn)在還不穩(wěn)定。

第三層是庫(kù)映射。自然語(yǔ)言里一句“用Hahn-Banach定理”，到了LEAN里不一定剛好有一個(gè)同名定理可以調(diào)用。庫(kù)里的定理可能叫另一個(gè)名字，前提寫法可能不同，結(jié)論形式也可能差一點(diǎn)。模型要找到能用的版本，還要補(bǔ)齊中間轉(zhuǎn)換。

第四層是證明重構(gòu)。人類證明經(jīng)常只寫主線，把大量計(jì)算、邊界條件和小引理留給讀者。LEAN不會(huì)替你腦補(bǔ)。很多時(shí)候，原論文的一段證明，形式化時(shí)要拆成一串新的lemma，證明順序也要重排。

最難的一層是上下文。論文里的一個(gè)符號(hào)，可能依賴前面幾十頁(yè)的約定；一個(gè)“顯然”，可能依賴作者所在領(lǐng)域的默認(rèn)技巧；一個(gè)“標(biāo)準(zhǔn)構(gòu)造”，可能根本沒(méi)有寫出來(lái)。autoformalization真正要處理的，是整篇論文背后的數(shù)學(xué)語(yǔ)境。

如果autoformalization做通，AI數(shù)學(xué)會(huì)發(fā)生質(zhì)變。過(guò)去一百年的論文、教材、講義和證明，都可以更快進(jìn)入機(jī)器可驗(yàn)證的世界。AI不再只是在mathlib里玩，它可以真正讀懂?dāng)?shù)學(xué)文獻(xiàn)的骨架。

但這一步現(xiàn)在還遠(yuǎn)遠(yuǎn)沒(méi)完全解決。自然語(yǔ)言數(shù)學(xué)太省略，庫(kù)里的形式化表達(dá)又太精確。把它翻成LEAN，需要做的遠(yuǎn)超語(yǔ)言轉(zhuǎn)換，更像是把一篇論文重新拆成定義、引理、依賴關(guān)系和可檢查步驟。

五、VC 砸錢賭的不是黎曼猜想

5.1 數(shù)學(xué)定理本身很難賣錢

很多人看到Axiom、Harmonic的估值，會(huì)本能地問(wèn)：證明數(shù)學(xué)定理怎么賺錢？

答案很直接：很難靠數(shù)學(xué)定理本身賺錢。

如果某家公司明天證明了黎曼猜想，數(shù)學(xué)界會(huì)震動(dòng)，媒體會(huì)刷屏，公司會(huì)收獲巨大聲譽(yù)。但這不是一個(gè)清晰的商業(yè)模式。沒(méi)有哪個(gè)客戶會(huì)因?yàn)槟阕C明了黎曼猜想，每年給你付幾千萬(wàn)美元訂閱費(fèi)。

數(shù)學(xué)定理的價(jià)值很奇怪。它一旦被證明，就屬于全人類知識(shí)。你可以因?yàn)檫@個(gè)成果拿獎(jiǎng)、拿名聲、拿學(xué)術(shù)地位，也可能因此吸引人才和資本。但它不像SaaS賬號(hào)，也不像API調(diào)用，很難按次收費(fèi)、按席位收費(fèi)、按年續(xù)費(fèi)。

這也是為什么Axiom和Harmonic雖然講數(shù)學(xué)，但資本真正看的不會(huì)是“證明多少個(gè)漂亮定理”。漂亮定理是展示能力的舞臺(tái)，商業(yè)化要落到另一個(gè)問(wèn)題：這些證明能力能不能變成別人愿意長(zhǎng)期付費(fèi)的可靠性服務(wù)？

換句話說(shuō)，數(shù)學(xué)本身是招牌，驗(yàn)證才是產(chǎn)品。

5.2 真正的市場(chǎng)在形式化代碼驗(yàn)證

VC真正看上的，是形式化驗(yàn)證。

AI寫代碼已經(jīng)變成巨大市場(chǎng)。Cursor、Claude Code、GitHub Copilot、OpenAI Codex這類工具正在把代碼生產(chǎn)速度拉上去。問(wèn)題是，AI寫的代碼經(jīng)常有bug。有些bug只是頁(yè)面錯(cuò)位，有些bug會(huì)變成安全漏洞、金融損失、自動(dòng)駕駛事故或醫(yī)療系統(tǒng)錯(cuò)誤。

傳統(tǒng)軟件工程靠測(cè)試。測(cè)試可以覆蓋很多情況，但它本質(zhì)上是抽樣。你測(cè)了1000個(gè)輸入，也不能證明第1001個(gè)輸入不會(huì)出事。形式化驗(yàn)證要解決的是另一類問(wèn)題：在數(shù)學(xué)意義上證明這段程序滿足某個(gè)規(guī)格。

這里要把“測(cè)試”和“證明”的差別說(shuō)清楚。

測(cè)試是在問(wèn)：我試過(guò)這些情況，它們都沒(méi)壞。形式化驗(yàn)證是在問(wèn)：在某個(gè)精確定義的范圍內(nèi)，這段程序?qū)λ星闆r都滿足規(guī)格。前者是經(jīng)驗(yàn)保證，后者是數(shù)學(xué)保證。

舉個(gè)很小的例子。一個(gè)轉(zhuǎn)賬函數(shù)，測(cè)試可以檢查100美元、0美元、負(fù)數(shù)輸入、余額不足等很多case。形式化驗(yàn)證想證明的是：不管輸入怎么變化，只要滿足前提條件，總金額不會(huì)憑空增加，賬戶余額不會(huì)變成非法狀態(tài)，權(quán)限條件不會(huì)被繞過(guò)。

這就是Menlo Ventures投Axiom時(shí)講的邏輯。Menlo的文章標(biāo)題很直白：AI會(huì)寫所有代碼，數(shù)學(xué)會(huì)證明它能工作。它們押注的是一個(gè)未來(lái)：代碼越來(lái)越多由AI生成，真正稀缺的東西變成“可信”。

Menlo文章里有一句判斷很關(guān)鍵：AI生成代碼看起來(lái)對(duì)，能編譯，經(jīng)常能跑，但這離“可證明正確”還很遠(yuǎn)。它們認(rèn)為這類問(wèn)題來(lái)自統(tǒng)計(jì)模型本身，很難靠下一個(gè)模型版本自動(dòng)消失。Axiom要做的，就是把AI代碼生成從“概率上靠譜”推進(jìn)到“關(guān)鍵部分可以被數(shù)學(xué)證明”。

金融系統(tǒng)、加密協(xié)議、航空航天、自動(dòng)駕駛、醫(yī)療設(shè)備、基礎(chǔ)設(shè)施軟件，這些地方錯(cuò)一次代價(jià)很高。如果AI能把形式化驗(yàn)證成本降下來(lái)，真正的市場(chǎng)會(huì)來(lái)自所有需要高可靠軟件的公司，數(shù)學(xué)家只是早期用戶。

Harmonic也在往這個(gè)方向走。它2025年12月發(fā)布Aristotle在VERINA Code Verification Benchmark上的結(jié)果，聲稱解決了189個(gè)形式化規(guī)格中的183個(gè)，完成率96.8%。這類benchmark的目標(biāo)已經(jīng)從數(shù)學(xué)競(jìng)賽題轉(zhuǎn)向了代碼和規(guī)格的一致性驗(yàn)證。

這說(shuō)明數(shù)學(xué)證明能力正在外溢。先在IMO、Putnam、mathlib里證明自己能推理，再把同一套能力遷移到代碼驗(yàn)證。真正的客戶不一定關(guān)心群論、數(shù)論和拓?fù)洌麄冴P(guān)心一件事：AI寫出來(lái)的關(guān)鍵代碼，能不能放心上線。

5.3 形式化驗(yàn)證過(guò)去為什么沒(méi)火

問(wèn)題是，形式化驗(yàn)證不是新東西。

它已經(jīng)存在幾十年，也確實(shí)有很多硬核成果。seL4微內(nèi)核就是經(jīng)典例子。它用形式化方法證明了操作系統(tǒng)內(nèi)核的關(guān)鍵正確性和安全性質(zhì)，被高安全系統(tǒng)反復(fù)引用。DARPA這些年也一直資助形式化方法，用在安全文檔解析、系統(tǒng)建模、高保證軟件等場(chǎng)景。

如果這東西這么好，為什么過(guò)去沒(méi)有大規(guī)模普及？

原因也很直接：太貴、太慢、太難用。

過(guò)去做形式化驗(yàn)證，往往需要懂軟件工程、懂?dāng)?shù)學(xué)、懂邏輯、懂證明工具的人。這樣的人本來(lái)就少，還貴。很多時(shí)候，寫規(guī)格、寫證明、維護(hù)證明的成本，甚至比寫代碼本身還高。Menlo那篇文章提到傳統(tǒng)形式化驗(yàn)證市場(chǎng)很小，一個(gè)原因就是它常常需要博士級(jí)專家，甚至可能出現(xiàn)“每一行代碼配很多行證明”的成本結(jié)構(gòu)。

工程團(tuán)隊(duì)也不喜歡這種工作方式。產(chǎn)品要上線，需求在變，代碼在改。只要代碼一改，證明可能也要跟著改。對(duì)大多數(shù)互聯(lián)網(wǎng)業(yè)務(wù)來(lái)說(shuō)，測(cè)試、監(jiān)控、灰度、回滾已經(jīng)夠用了。它們寧愿承受一點(diǎn)線上bug，也不愿為數(shù)學(xué)意義上的正確付出巨大成本。

所以形式化驗(yàn)證過(guò)去一直停留在高價(jià)值、高風(fēng)險(xiǎn)、強(qiáng)監(jiān)管的地方。航空航天、軍工、加密、操作系統(tǒng)內(nèi)核、金融基礎(chǔ)設(shè)施，這些地方值得做；普通業(yè)務(wù)系統(tǒng)大多不會(huì)做。

AI帶來(lái)的變量，是成本結(jié)構(gòu)可能變了。

如果模型能自動(dòng)寫規(guī)格、自動(dòng)補(bǔ)證明、自動(dòng)修復(fù)證明失敗的地方，形式化驗(yàn)證的門檻就會(huì)下降。過(guò)去需要頂級(jí)專家做幾周的事，未來(lái)可能變成工程師點(diǎn)幾次、模型跑一會(huì)兒、系統(tǒng)給出證明和反例。

這正是Axiom、Harmonic這類公司最想講的故事：形式化驗(yàn)證過(guò)去是少數(shù)專家手里的奢侈品，它們?cè)噲D把它變成AI時(shí)代的軟件基礎(chǔ)設(shè)施。

5.4 Agent 的信任層和估值泡沫

還有一層更大的想象空間，是AI agent的信任層。未來(lái)如果agent能替你轉(zhuǎn)賬、下單、改數(shù)據(jù)庫(kù)、部署代碼、簽合同，那么它每次行動(dòng)前都需要某種可驗(yàn)證約束。它不能只是“我覺(jué)得這樣沒(méi)問(wèn)題”，它要能證明這一步不違反規(guī)則。

這就是數(shù)學(xué)證明技術(shù)可能商業(yè)化的地方?？蛻舨辉跀?shù)學(xué)系，而在軟件、金融、安全、機(jī)器人和AI平臺(tái)。

比如一個(gè)代碼agent要改支付系統(tǒng)，它最好能證明自己沒(méi)有改變金額守恒；一個(gè)數(shù)據(jù)庫(kù)agent要批量遷移數(shù)據(jù)，它最好能證明關(guān)鍵字段不會(huì)丟；一個(gè)交易agent要執(zhí)行策略，它最好能證明不會(huì)突破風(fēng)控限制；一個(gè)機(jī)器人agent要操作物理設(shè)備，它最好能證明某些安全邊界不會(huì)被越過(guò)。

這時(shí)候，證明技術(shù)就不只是“檢查代碼對(duì)不對(duì)”。它變成agent行動(dòng)前的護(hù)欄。agent越能做事，驗(yàn)證層越值錢。

但我對(duì)這里的估值仍然保持懷疑。

形式化驗(yàn)證過(guò)去幾十年一直是好東西，但始終沒(méi)有大規(guī)模普及。大家知道它嚴(yán)謹(jǐn)，真正卡住普及的是貴、慢、難用，以及對(duì)工程團(tuán)隊(duì)要求太高。AI可以降低門檻，但能不能降低到普通公司愿意買單，還沒(méi)有答案。

很多公司可能會(huì)選擇另一條便宜路線：更強(qiáng)的模型，加更多測(cè)試，加灰度發(fā)布，加監(jiān)控回滾。它們不一定愿意為了“數(shù)學(xué)意義上的正確”多付幾十倍成本。只有當(dāng)事故代價(jià)足夠高，或者監(jiān)管要求足夠硬，形式化驗(yàn)證才會(huì)從高級(jí)玩具變成預(yù)算項(xiàng)。

所以VC賭的不是“AI證明黎曼猜想后賣門票”。他們賭的是兩件事。

第一，AI生成代碼和agent行動(dòng)會(huì)變得越來(lái)越多，風(fēng)險(xiǎn)也會(huì)越來(lái)越大。第二，AI本身能把形式化驗(yàn)證的成本打下來(lái)。前者創(chuàng)造需求，后者降低供給成本。兩件事同時(shí)成立，這個(gè)市場(chǎng)才會(huì)打開(kāi)。

如果只有前者，沒(méi)有后者，形式化驗(yàn)證還是太貴。如果只有后者，沒(méi)有足夠高風(fēng)險(xiǎn)的應(yīng)用，客戶也不急著買單。這就是這條賽道最核心的商業(yè)不確定性。

六、三年內(nèi)能看到什么，別期待什么

6.1 幾乎確定：庫(kù)會(huì)變大，工具會(huì)進(jìn)日常

未來(lái)三年，最確定的變化是mathlib會(huì)繼續(xù)長(zhǎng)大。

這件事聽(tīng)起來(lái)不刺激，但它最穩(wěn)。AI for Math Fund、LEAN FRO、Harmonic的捐贈(zèng)和贊助、大學(xué)里的形式化項(xiàng)目，都會(huì)把更多現(xiàn)代數(shù)學(xué)搬進(jìn)LEAN。代數(shù)、分析、數(shù)論、拓?fù)?、范疇論里還會(huì)有更多定義、定理和證明被寫成機(jī)器能檢查的形式。

這個(gè)過(guò)程很慢，但很扎實(shí)。每搬進(jìn)去一塊，AI能使用的工具箱就大一圈。今天模型卡住，可能只是因?yàn)槟硞€(gè)舊定理還沒(méi)進(jìn)庫(kù)，或者進(jìn)庫(kù)了但名字、形式、依賴關(guān)系很難找。三年后，這類低級(jí)摩擦?xí)俸芏唷?/p>

第二個(gè)確定變化，是autoformalization會(huì)明顯進(jìn)步。

它未必能一鍵把論文變成LEAN證明，但會(huì)先在更窄的場(chǎng)景里變好。比如把教材里的標(biāo)準(zhǔn)定理形式化，把本科生證明題翻成LEAN，把論文里的局部lemma翻成機(jī)器可檢查版本。這些小場(chǎng)景一旦跑順，就會(huì)慢慢擴(kuò)大到更復(fù)雜的論文片段。

數(shù)學(xué)家也會(huì)越來(lái)越多地把AI當(dāng)成日常工具。它不一定替你想出核心思想，但可以幫你查庫(kù)、補(bǔ)lemma、驗(yàn)證邊界條件、找反例、把一個(gè)證明草稿改成更嚴(yán)謹(jǐn)?shù)男问?。陶哲軒談AI時(shí)更偏向這個(gè)方向：AI像一個(gè)能協(xié)作的初級(jí)助手，而不是按一下按鈕就給出深theorem的神機(jī)。

這種工具進(jìn)入日常以后，數(shù)學(xué)家的工作方式會(huì)變。以前你要花一天查一個(gè)庫(kù)里有沒(méi)有某個(gè)lemma，以后可能幾分鐘就能問(wèn)出來(lái)。以前一個(gè)證明草稿有一堆邊界條件，AI可以先幫你試著形式化，告訴你哪里少了前提。它像一個(gè)不知疲倦的研究助理，水平未必最高，但能不斷試錯(cuò)。

高端軟件驗(yàn)證也大概率會(huì)起量。金融、加密、航空、自動(dòng)駕駛、醫(yī)療設(shè)備和AI基礎(chǔ)設(shè)施里，會(huì)有一批客戶愿意為更強(qiáng)保證付費(fèi)。Axiom、Harmonic這類公司如果能先在這里落地，估值故事就不只是故事。

但這里的落地不會(huì)是全行業(yè)鋪開(kāi)。更可能先從小模塊開(kāi)始，比如關(guān)鍵函數(shù)、加密協(xié)議、智能合約、風(fēng)控規(guī)則、數(shù)據(jù)庫(kù)遷移腳本、agent行動(dòng)約束。先證明最危險(xiǎn)的局部，再慢慢擴(kuò)大。

6.2 可能發(fā)生：中等難度開(kāi)放問(wèn)題被 AI 補(bǔ)上

比較可能發(fā)生的標(biāo)志性事件，是AI在某個(gè)具體子領(lǐng)域里解決一個(gè)有學(xué)術(shù)分量的開(kāi)放問(wèn)題。這個(gè)問(wèn)題大概率不會(huì)是黎曼猜想那種全人類盯了一百多年的超級(jí)難題，而是某個(gè)邊界清晰、可以形式化、已有大量工具可用的中等難度問(wèn)題。

這類問(wèn)題有幾個(gè)特征。背景已經(jīng)比較成熟，相關(guān)定義和定理大多能形式化；問(wèn)題本身邊界清楚，不需要發(fā)明全新的語(yǔ)言；證明可能需要大量搜索、拆case、組合已有工具。人類數(shù)學(xué)家能看出方向，但細(xì)節(jié)太多，或者某個(gè)關(guān)鍵連接長(zhǎng)期沒(méi)人撞上。

Axiom聲稱已經(jīng)在類似方向上拿到過(guò)結(jié)果，Harmonic也在宣傳它解決過(guò)未解Erdos問(wèn)題的形式化版本。哪怕對(duì)這些宣傳保持謹(jǐn)慎，也能看出方向：AI最先可能補(bǔ)上的，是那些“理論框架已有、證明空間巨大、需要大量試錯(cuò)”的問(wèn)題。

這類事件一旦發(fā)生，媒體標(biāo)題一定會(huì)寫成“AI擊敗數(shù)學(xué)家”。真實(shí)情況會(huì)復(fù)雜得多。很可能是人類提出問(wèn)題、整理背景、搭好LEAN環(huán)境，AI在其中補(bǔ)上關(guān)鍵證明或大規(guī)模搜索。它仍然值得重視，但不等于數(shù)學(xué)家失業(yè)。

更準(zhǔn)確的說(shuō)法，可能是“AI參與解決了一個(gè)開(kāi)放問(wèn)題”。人類負(fù)責(zé)選題、建模、解釋結(jié)果、檢查數(shù)學(xué)意義；AI負(fù)責(zé)在形式化空間里跑大量搜索，找到人類沒(méi)有及時(shí)發(fā)現(xiàn)的連接。

6.3 別期待：黎曼猜想級(jí)別還沒(méi)到時(shí)候

三年內(nèi)基本別期待AI解決黎曼猜想、P vs NP、Navier-Stokes這種級(jí)別的問(wèn)題。

這些問(wèn)題難在需要新的概念、新的語(yǔ)言、新的理論框架，單純加算力和數(shù)據(jù)很難解決。人類數(shù)學(xué)史上真正的大突破，往往不靠把舊工具用得更快，而靠發(fā)明新的看法。AI現(xiàn)在更像一個(gè)極強(qiáng)的證明搜索和形式化工具，還不像一個(gè)能獨(dú)立發(fā)明新數(shù)學(xué)語(yǔ)言的研究者。

超級(jí)難題還有一個(gè)現(xiàn)實(shí)問(wèn)題：它們周圍的形式化基礎(chǔ)不一定夠。你要讓AI解決黎曼猜想，不只是把一句“證明黎曼猜想”丟給模型。你需要把相關(guān)的解析數(shù)論、復(fù)分析、譜理論、代數(shù)幾何或者其他可能路線，盡量放進(jìn)可用的形式化環(huán)境里。這個(gè)地基本身就是巨大工程。

而且超級(jí)難題通常需要新的結(jié)構(gòu)，單純長(zhǎng)計(jì)算不夠。人類歷史上的大定理，很多時(shí)候靠的是換一張地圖，舊路加速只能解決一部分問(wèn)題。AI能不能發(fā)明這種地圖，現(xiàn)在還沒(méi)有證據(jù)。

所以三年內(nèi)更現(xiàn)實(shí)的邊界是：AI在已有理論框架里變得很強(qiáng)，在形式化證明搜索里變得很強(qiáng)，在局部引理和中等問(wèn)題上越來(lái)越有用。但“獨(dú)立發(fā)明新數(shù)學(xué)語(yǔ)言、解決最頂級(jí)難題”，還不是當(dāng)前最該下注的預(yù)期。

6.4 公司結(jié)局：大廠收購(gòu)會(huì)比數(shù)學(xué)突破更早

公司層面倒是很可能出現(xiàn)大額并購(gòu)。OpenAI、Google、Anthropic、微軟、Meta這類公司都需要更強(qiáng)推理和驗(yàn)證能力。對(duì)它們來(lái)說(shuō)，幾十億美元收購(gòu)一個(gè)頂級(jí)形式化推理團(tuán)隊(duì)，不是離譜劇本。

原因很簡(jiǎn)單。大模型公司都在往agent、coding、科研、企業(yè)自動(dòng)化走。模型越能行動(dòng)，越需要驗(yàn)證。誰(shuí)能把“模型輸出”變成“可檢查輸出”，誰(shuí)就能在高價(jià)值場(chǎng)景里多賣一層信任。

所以Axiom、Harmonic這類公司，未必一定要先證明世界級(jí)數(shù)學(xué)難題，才有商業(yè)價(jià)值。只要它們證明自己能穩(wěn)定生成可驗(yàn)證代碼、可驗(yàn)證推理、可驗(yàn)證agent約束，就已經(jīng)足夠讓大廠動(dòng)心。

但并購(gòu)不是技術(shù)成功的證明。它只說(shuō)明大廠相信這條能力不能缺席。

另一個(gè)可能發(fā)生的局面，是生態(tài)分化。閉源公司做大模型和高端客戶，開(kāi)源社區(qū)繼續(xù)建設(shè)LEAN、mathlib、LeanDojo、autoformalization工具。最后真正推動(dòng)行業(yè)的，可能會(huì)是閉源模型、開(kāi)源庫(kù)、數(shù)學(xué)家社區(qū)和企業(yè)驗(yàn)證需求一起往前推。

所以未來(lái)三年，我會(huì)把預(yù)期放在三個(gè)層級(jí)：基礎(chǔ)設(shè)施一定會(huì)變厚，數(shù)學(xué)家日常工具會(huì)變好，高風(fēng)險(xiǎn)軟件驗(yàn)證會(huì)開(kāi)始試水。至于AI獨(dú)立成為研究級(jí)數(shù)學(xué)家，時(shí)間表還要往后放。

七、數(shù)學(xué)是 AI 的照妖鏡

7.1 數(shù)學(xué)的規(guī)則比藝術(shù)硬得多

回到開(kāi)頭的Axiom故事，一個(gè)資深數(shù)論學(xué)家離開(kāi)大學(xué)，加入一家年輕AI數(shù)學(xué)公司。這件事真正有意思的地方，不只是“老教授去了創(chuàng)業(yè)公司”，也不只是“2億美元融資”。它說(shuō)明AI終于走到一個(gè)很難糊弄的場(chǎng)景里。

過(guò)去幾年，AI在藝術(shù)、寫作、圖片、視頻上給人的沖擊很大。但這些領(lǐng)域有一個(gè)共同特點(diǎn)：標(biāo)準(zhǔn)比較軟。你說(shuō)這張圖好，我可以說(shuō)它不夠高級(jí)；你說(shuō)一段文案普通，我可以說(shuō)它適合轉(zhuǎn)化；你說(shuō)一段視頻怪，我可以說(shuō)這是風(fēng)格。

數(shù)學(xué)不吃這一套。

一個(gè)證明要么成立，要么不成立。一個(gè)LEAN證明通過(guò)了，就是通過(guò)了。沒(méi)通過(guò)，再像論文也沒(méi)有用。數(shù)學(xué)不給模型留“語(yǔ)氣很自信”“看起來(lái)很合理”“大概差不多”的空間。

這就是AI證明數(shù)學(xué)最迷人的地方。它不靠情緒，不靠風(fēng)格，不靠“像不像”。它逼AI面對(duì)一個(gè)硬問(wèn)題：你到底會(huì)不會(huì)推理？

7.2 數(shù)學(xué)家不會(huì)被一鍵替代

所以我不認(rèn)為AI三年內(nèi)會(huì)變成高斯、歐拉，也不認(rèn)為數(shù)學(xué)家會(huì)被一鍵替代。

數(shù)學(xué)家的工作并不只是把一段證明從A推到B。真正難的地方，經(jīng)常在證明之前：提出好問(wèn)題，選擇好定義，判斷一個(gè)方向有沒(méi)有價(jià)值，決定該在哪個(gè)理論框架里看這個(gè)問(wèn)題。很多時(shí)候，一個(gè)定義選錯(cuò)了，后面證明再努力也會(huì)很難走。

AI現(xiàn)在更像一個(gè)很強(qiáng)的加速器。它可以幫你查mathlib，補(bǔ)lemma，驗(yàn)證邊界條件，找反例，把一個(gè)證明草稿改成更嚴(yán)謹(jǐn)?shù)男问健Ｋ绕渖瞄L(zhǎng)吃掉那些枯燥、細(xì)碎、可驗(yàn)證、需要大量試錯(cuò)的部分。

這已經(jīng)足夠大了。

如果過(guò)去一個(gè)數(shù)學(xué)家要花幾周把一個(gè)證明形式化，以后可能只需要幾小時(shí)或幾天。如果過(guò)去一個(gè)研究生要反復(fù)查庫(kù)、試tactic、補(bǔ)小引理，以后AI可以承擔(dān)大部分機(jī)械勞動(dòng)。數(shù)學(xué)家的時(shí)間會(huì)更多地花在上游：?jiǎn)栴}、結(jié)構(gòu)、定義、路線和解釋。

換句話說(shuō)，數(shù)學(xué)家不會(huì)立刻消失，但數(shù)學(xué)家的工作流會(huì)變。越靠近“機(jī)械化證明勞動(dòng)”的部分，越容易被AI吃掉；越靠近“提出什么問(wèn)題、為什么值得做、用什么語(yǔ)言看它”的部分，越仍然需要人。

7.3 AI 終于遇到不能糊弄的考試

從Logic Theorist到AlphaProof，從希爾伯特的形式化夢(mèng)想，到今天的LEAN和mathlib，AI繞了一大圈又回到原點(diǎn)。區(qū)別在于，這一次它不再只拿著手寫規(guī)則和小搜索樹(shù)，而是帶著神經(jīng)網(wǎng)絡(luò)、強(qiáng)化學(xué)習(xí)、海量數(shù)據(jù)和真正可驗(yàn)證的數(shù)學(xué)庫(kù)。

這條路最后能走多遠(yuǎn)，現(xiàn)在沒(méi)人知道。黎曼猜想可能還很遠(yuǎn)，研究級(jí)數(shù)學(xué)也不會(huì)被一夜之間自動(dòng)化?？芍辽儆幸患乱呀?jīng)發(fā)生：AI終于開(kāi)始接受一種它無(wú)法靠話術(shù)混過(guò)去的考試。

這個(gè)考試的結(jié)果，會(huì)反過(guò)來(lái)影響很多領(lǐng)域。

如果AI能在數(shù)學(xué)里學(xué)會(huì)“可驗(yàn)證推理”，它就不只是在數(shù)學(xué)里有用。代碼驗(yàn)證、科學(xué)推理、agent安全、金融風(fēng)控、機(jī)器人控制，都需要類似能力。模型不能只給一個(gè)看起來(lái)合理的答案，還要能給出可以檢查的理由。

這也是為什么VC愿意給Axiom、Harmonic這種公司高估值。資本當(dāng)然會(huì)講故事，也會(huì)制造泡沫。但泡沫背后有一個(gè)真實(shí)問(wèn)題：當(dāng)AI開(kāi)始寫代碼、做決策、操作系統(tǒng)，人類需要某種硬驗(yàn)證機(jī)制。數(shù)學(xué)證明是目前最硬的一種。

所以這篇文章的問(wèn)題，不能只理解成“AI能不能發(fā)現(xiàn)新定理”。更準(zhǔn)確地說(shuō)，它在問(wèn)：AI能不能從生成漂亮答案，走向生成可信答案？

如果答案是能，那數(shù)學(xué)只是第一塊試金石。如果答案是不能，那數(shù)學(xué)會(huì)成為AI能力邊界最誠(chéng)實(shí)的照妖鏡。

作者其它文章

? 手把手教你分析：你會(huì)被AI取代嗎?

? 一篇文章講清大語(yǔ)言模型發(fā)展史

? 氣吞萬(wàn)里如虎：回顧十九世紀(jì)的數(shù)學(xué)英豪們

? Vibe Reading：AI 時(shí)代讀書(shū)的系統(tǒng)化方法

? 長(zhǎng)篇分析：Manus 案折射出的中國(guó) AI 創(chuàng)業(yè)生態(tài)

? 別再被 AI 新詞繞暈了：Prompt、Context、Agent 背后的工程主線

? 兩萬(wàn)字科普：AI 為什么會(huì)編程——原理、歷史與未來(lái)

? 兄弟們，真·Vibe Writing 時(shí)代到來(lái)了

? 全網(wǎng)最詳細(xì)的AI學(xué)習(xí)路線圖

? 每個(gè)人都應(yīng)該使用的三個(gè)最有用的 Claude Skill

? SpaceX 立志傳（一）：賭上全部的最后一次發(fā)射

? 估值290億美元的套殼公司，正在被自己的房東殺死

? 黃仁勛和主持人吵紅了臉：芯片封鎖中國(guó)，美國(guó)到底能不能打贏？

? AI將如何顛覆教育，普通人又應(yīng)該如何搶奪教育新的生態(tài)位

? 學(xué)物理的八方英雄們，物理學(xué)已死，請(qǐng)轉(zhuǎn)行搞AI

? 不會(huì)編程、沒(méi)有融資、沒(méi)有員工，他怎么一個(gè)人做到年入2000萬(wàn)

? 兄弟們想清楚：究竟是你為X打工，還是X為你打工？

? 一人公司盈利四億美元：是騙子，還是可復(fù)制的紅利？

? 2026第一季度大裁員，AI是背鍋俠嗎？

? 重返星辰大海：這次繞月飛行有意義嗎？

? 張雪峰在美國(guó)為什么無(wú)法成功

? 2026 企業(yè)尸檢報(bào)告：不用AI，你的公司能活過(guò)今年嗎？

? 兄弟們，我創(chuàng)業(yè)失敗了，人生完整了

本文參考文獻(xiàn)

? 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