陶哲軒12年前的預言，現(xiàn)在AI幫他兌現(xiàn)了

• 聞樂 發(fā)自 凹非寺
  量子位 | 公眾號 QbitAI

事實證明，菲爾茲獎得主有時候也兼職預言家。

12年前，陶哲軒在首屆數(shù)學突破獎的臺上拋出的一句預言，被視作天方夜譚：

• 將來有一天，我們或許不再用LaTeX撰寫論文，而是使用計算機能理解的的形式化語言。

那一年，Transformer還沒誕生，ChatGPT更是連影子都沒有。

沒想到，回旋鏢正中靶心。過去這一年，AI在數(shù)學領域突然開始瘋狂提速。

從OpenAI解決開放問題，到DeepMind批量攻克數(shù)學猜想，越來越多數(shù)學證明被寫進形式化系統(tǒng)，交給計算機自動驗證。

回望來路，最早看清風向、親自下場實踐的人，就是陶哲軒。

十年間，他先后推進大規(guī)模協(xié)作數(shù)學、Lean形式化證明、又發(fā)起Equational Theories項目，面對2200萬個數(shù)學問題，依靠「AI+人類協(xié)作」，短短48小時就攻克大半。

項目在AI助力下效率拉滿，很多時候連他本人都不用插手了。

實際上，陶哲軒這也是用實際行動證明，最好的預測未來，就是親手把它創(chuàng)造出來。

神童，但更迷戀協(xié)作

說起陶哲軒，很多人第一反應是那串傳奇經(jīng)歷：

2歲時教比自己大的孩子數(shù)數(shù)，7歲開始接觸微積分，10歲成為國際數(shù)學奧林匹克史上最年輕的銅牌得主，24歲成為UCLA歷史上最年輕的終身教授之一，31歲拿下菲爾茲獎。

72歲的保羅?埃爾德什與10歲的陶哲軒 圖源：Quantamagazine

在大眾印象里，這樣的人往往屬于“天才獨行俠”。

但陶哲軒本人恰恰相反。

相比于孤軍奮戰(zhàn)，他一直對另一件事更感興趣：

數(shù)學家能不能像開源軟件開發(fā)者一樣協(xié)作？

一個人知道A，一個人知道B，如果把兩個人的知識拼起來，會不會出現(xiàn)單個人想不到的新東西？

這種想法后來深刻影響了他的整個職業(yè)生涯。

2009年，他參與了Polymath項目，一個把數(shù)學協(xié)作搬上公開論壇的實驗。

在這個項目里，任何人都可以登錄，認領子問題，提交思路，群策群力。

原本需要少數(shù)專家花費數(shù)月甚至數(shù)年完成的問題，在公開協(xié)作模式下被快速推進。

這次實驗最終成功解決了一個組合數(shù)學問題，證明了大規(guī)模協(xié)作在數(shù)學上不是空想。

Polymath成功了，但陶哲軒很快發(fā)現(xiàn)一個更大的問題：

所有的錯誤核查，都壓在核心負責人身上。

參與者越多，審核壓力越大；協(xié)作規(guī)模越大，組織成本越高。

沒有自動驗證工具，人工糾錯的速度永遠跟不上協(xié)作的規(guī)模。協(xié)作數(shù)學的上限，被壓住了。

要突破這道天花板，必須找到別的路。

2014年，他在首屆突破獎的臺上，描述了自己眼中的未來數(shù)學，也就是三個當時聽起來不太靠譜的預言：

• 數(shù)百人規(guī)模的大規(guī)模數(shù)學協(xié)作會成為常態(tài)；
• 計算機將能自動驗證數(shù)學證明；
• LaTeX會被機器能讀懂的形式化語言所取代。

今天看，這三個判斷幾乎對應了AI數(shù)學發(fā)展的全部主線。

但放在當時，它們聽起來過于超前。

雖然Polymath證明了協(xié)作數(shù)學行得通，但如果不能把“驗證”這件事自動化，數(shù)學研究很難真正實現(xiàn)規(guī)模化協(xié)作。

而他等待的答案，最終出現(xiàn)在一種名叫Lean的工具身上。

預言說了十年，他決定親自試試

轉(zhuǎn)機出現(xiàn)在2023年。

那一年，陶哲軒在一次交流中認識了數(shù)學家Kevin Buzzard，這位也是Lean的早期推廣者。

Lean是一套交互式定理證明系統(tǒng)，用形式化語言描述數(shù)學證明，讓計算機逐行驗證每一步的邏輯。

這套理念恰好擊中了陶哲軒多年來思考的問題，于是，在Buzzard的鼓勵下，48歲的陶哲軒決定親自下場實踐。

2023年10月9日，他在社交媒體上發(fā)了條狀態(tài)：

• 我決定終于開始學習Lean4交互式證明系統(tǒng)了（必要時使用AI協(xié)助）。

這位菲爾茲獎得主原本覺得，這不會太難，于是挑了一道關于麥克勞林不等式的問題作為練手項目，打算以此為素材，嘗試用Lean完成證明形式化。

他先按傳統(tǒng)寫法完成 10頁手寫風格證明，再著手將其轉(zhuǎn)譯為Lean代碼。按照他的估計，大概一周左右就能搞定。

然后，他碰壁了。

上手后他發(fā)現(xiàn)，形式化證明和寫數(shù)學論文是兩種完全不同的思維模式。

在傳統(tǒng)論文里，一句“三個大于1的數(shù)相加大于等于3”幾乎沒人會多看一眼，但Lean不行：

你必須明確告訴系統(tǒng)你引用的結(jié)論來自哪里？對應哪一個引理？

很多看似顯然的步驟，都需要補上大量形式化細節(jié)，原本幾行紙面推導，很容易變成數(shù)百行代碼。

一個月后，陶哲軒終于完成自己的第一個正式化證明。

雖然代碼并不優(yōu)雅，但從那一天開始，他真正成為了形式化數(shù)學社區(qū)的一員。

PFR項目：預言第一次落地

在他學習Lean不久后，就出現(xiàn)了一個新的機會。

2023年11月9日，陶哲軒和合作者Ben Green、Tim Gowers等人完成了一篇關于PFR猜想的論文。

這是一個關于集合加法結(jié)構(gòu)的數(shù)論命題，此前懸而未決多年。

論文寫完了，但他沒停。接著，他在Lean社區(qū)發(fā)了一篇帖子：

• 大家好，我準備啟動一個項目，把PFR猜想的最新證明在Lean4里正式化……歡迎任何人參與。

這次和Polymath最大的不同在于，Lean負責審查

這一次，他把論文拆成了一塊塊可以獨立認領的子任務，開放給全球社區(qū)。

每個人完成自己的一塊，系統(tǒng)自動核驗，通過了才能合并進主線。

結(jié)果全程僅三周，所有形式化工作全部完成。

甚至，陶哲軒發(fā)布了一個額外的小任務，不到1小時就有社區(qū)成員完成并提交。

這也是他第一次看到自己十多年前設想的協(xié)作數(shù)學模式，真的能運轉(zhuǎn)起來。

2200萬種數(shù)學關系，48小時確定大半

嘗到甜頭之后，他把賭注押得更大了。

2024年9月25日，陶哲軒發(fā)起了Equational Theories項目，目標是系統(tǒng)性地確定約2200萬個代數(shù)等式之間的邏輯蘊含關系。

簡單說，就是搞清楚哪些方程式能從哪些方程式推導出來。

這次陶哲軒用上了全新組合：AI幫忙寫證明，Lean負責檢查對錯，全球志愿者社區(qū)分頭攻克具體難題，三方協(xié)同推進工作。

自動化證明助手工作流程 圖源：Quantamagazine

這次結(jié)果出得更快！48小時內(nèi)，大規(guī)模篩選基本完成，大量問題已經(jīng)解決在望。

前9天，整體進度已推進到99.866%，第57天，主項目宣告基本完工，只剩162個蘊含關系等待收尾。

甚至，這個項目還在過程中催生了一個全新的數(shù)學概念magma cohomology（原群上同調(diào)）

這個概念是為無公理約束的原群量身打造的上同調(diào)理論，核心是定義了依賴等式的上同調(diào)群H1、H2，用于分類原群擴張、構(gòu)造反例、區(qū)分不同原群，是經(jīng)典群上同調(diào)的推廣，用來研究最一般的代數(shù)結(jié)構(gòu)。

除此之外，Equational Theories項目展現(xiàn)出的自主運轉(zhuǎn)能力，也讓陶哲軒欣喜。

依托AI輔助與自動化核驗，即便他不全程跟進，各項工作也能穩(wěn)步推進。

過去兩年里，陶哲軒已經(jīng)越來越頻繁地把AI納入自己的研究流程，也不斷建議年輕學者要掌握與AI協(xié)作的能力。

從陶哲軒身上可以看到的是，最好的預言家，其實是先行者——

不止于預判未來，親身實踐，一步步把曾經(jīng)的設想變?yōu)楝F(xiàn)實。

如今，這位先行者也已經(jīng)成為AI數(shù)學最堅定的布道者。

[1]https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/
[2]https://terrytao.wordpress.com/2023/11/
[3]https://gowers.wordpress.com/2009/03/10/