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

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

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

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

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

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

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

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

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

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

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

神童，但更迷戀協作

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

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

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

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

但陶哲軒本人恰恰相反。

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

數學家能不能像開源軟件開發者一樣協作？

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

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

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

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

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

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

Polymath成功了，但陶哲軒很快發現一個更大的問題：

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

參與者越多，審核壓力越大；協作規模越大，組織成本越高。

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

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

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

• 數百人規模的大規模數學協作會成為常態；
• 計算機將能自動驗證數學證明；
• LaTeX會被機器能讀懂的形式化語言所取代。

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

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

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

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

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

轉機出現在2023年。

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

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

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

2023年10月9日，他在社交媒體上發了條狀態：

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

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

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

然后，他碰壁了。

上手后他發現，形式化證明和寫數學論文是兩種完全不同的思維模式。

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

你必須明確告訴系統你引用的結論來自哪里？對應哪一個引理？

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

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

雖然代碼并不優雅，但從那一天開始，他真正成為了形式化數學社區的一員。

PFR項目：預言第一次落地

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

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

這是一個關于集合加法結構的數論命題，此前懸而未決多年。

論文寫完了，但他沒停。接著，他在Lean社區發了一篇帖子：

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

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

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

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

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

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

這也是他第一次看到自己十多年前設想的協作數學模式，真的能運轉起來。

2200萬種數學關系，48小時確定大半

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

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

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

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

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

這次結果出得更快！48小時內，大規模篩選基本完成，大量問題已經解決在望。

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

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

這個概念是為無公理約束的原群量身打造的上同調理論，核心是定義了依賴等式的上同調群H1、H2，用于分類原群擴張、構造反例、區分不同原群，是經典群上同調的推廣，用來研究最一般的代數結構。

除此之外，Equational Theories項目展現出的自主運轉能力，也讓陶哲軒欣喜。

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

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

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

不止于預判未來，親身實踐，一步步把曾經的設想變為現實。

如今，這位先行者也已經成為AI數學最堅定的布道者。

[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/