陶哲軒談AI與形式化：數學研究的范式革命已經開始

近日，Math Inc. 與知名數學家陶哲軒進行了一場深入對話。作為 2006 年菲爾茲獎得主，他近年來在形式化數學與 AI 輔助證明領域的探索引發了學界廣泛關注。

從 2023 年底領導團隊在三周內完成多項式 Freiman-Ruzsa 猜想（Polynomial Freiman-Ruzsa Conjecture，PFR）的 Lean 形式化驗證，到 2024 年發起的“等式理論計劃”（Equational Theories Project），陶哲軒正在身體力行地推動一場數學研究范式的變革。這次對話中，他坦誠地分享了自己對形式化工具、AI 技術以及數學未來的思考。

（來源：Youtube）

他的核心觀點包括：

一、形式化正在改變數學寫作和思維方式。Lean 等工具迫使數學家更清晰地定義概念、檢驗假設，能自動發現“你其實從沒用過這個假設”——這有時帶來真正的數學進展。

二、形式化讓證明修改變得極其高效。PFR 猜想的形式化證明從 C=12 更新到 C=11，傳統方式可能需要再花三周，但在 Lean 中只用了一天。

三、數學研究可以像軟件工程一樣分工協作。不是每個人都需要懂 Lean、懂數學、懂 GitHub——只需要重疊的技能組合。這將讓更多“數學愛好者”參與前沿研究。

四、解析數論是自動化的理想目標。該領域約 70% 的工作是繁瑣的常數計算和參數匹配，一旦形式化，就能像 Excel 一樣自動更新——有人證明了新邊界，整個領域的相關結果可在幾分鐘內同步更新。

五、形式化建立了新的信任基礎設施。傳統數學依賴“圈子”和聲譽來判斷結果可靠性；有了 Lean 驗證，你可以使用素未謀面者的結果。

以下是對話全文。

問：你是從什么時候開始對機器輔助證明產生興趣的？

陶哲軒：回顧整個職業生涯，我始終覺得我們做數學的方式缺少了某些東西。研究一個數學問題時，我們追求的是那個能解鎖答案的精妙想法，但在抵達那個時刻之前，有大量瑣碎的工作需要完成——文獻綜述、技術細節調整。你在另一篇論文里發現一個有價值的技巧，想應用到自己的問題上，卻發現所有的輸入條件都略有出入，于是不得不手工調整論證、反復計算。這些工作當然是有意義的，能幫助建立直覺，但很多時候純粹是苦力活。我以前也嘗試過寫一些小型計算器來加速部分計算，但當時技術尚未成熟。

大約兩年前，我們在 IPAM（Institute for Pure and Applied Mathematics，純粹與應用數學研究所）舉辦了一場機器輔助證明的會議，我是組織者之一。在那里，我們接觸到了各種前沿嘗試，SAT 求解器、計算機輔助軟件包、大語言模型等等。ChatGPT 剛剛問世，Lean 也在蓬勃發展。突然間，許多原本遙不可及的事情變得觸手及極，整個領域正在經歷某種覺醒。

Peter Scholze 剛剛完成了一個歷時 18 個月的項目，用 Lean 形式化了他的一個重要定理：液態張量實驗（Liquid Tensor Experiment）。一個定理，18 個月，20 余位協作者。這在當時已被視為重大突破，因為 20 世紀的形式化項目往往需要數十年才能完成。速度的提升部分歸功于我們學會了使用軟件工程的工具——GitHub、更智能的項目組織方式。

圖丨 Peter Scholze（來源：WikiPedia）

問：那次會議促使你開始學習 Lean？

陶哲軒：那次會議之后，我對 AI 和形式化都產生了濃厚興趣，并確信這就是數學的未來方向。我開始接受采訪，四處談論這些想法。但到了某個節點，光說不練是不行的，必須真正動手。于是我開始學習 Lean，大約花了一個月時間。這個過程其實相當有趣，讓我想起當年撰寫本科實分析教材的經歷——從自然數的構造講起，把每一個細節都處理得完全嚴謹。使用 Lean 的感覺很像在玩電子游戲。Kevin Buzzard 曾說 Lean 是“世界上最好的電子游戲”，對某類人來說確實極易上癮。

而在過去一年里，大語言模型的能力突飛猛進，已經能夠自動形式化單個證明步驟，大幅減輕了形式化過程中的繁瑣工作。現在甚至可以實時進行形式化，這打開了無數新的可能性。

問：我在學習形式化證明的過程中有一個深刻體會：我逐漸意識到自己其實從未真正學會清晰地思考數學論證。高等數學的證明中似乎存在某種約定俗成的模糊性。隨著你越來越深入地接觸形式化，你對自身數學認知的理解是否也發生了變化？

陶哲軒：確實有所改變，尤其體現在寫論文的方式上。我現在能夠察覺到那些“隱形假設”，那些我們習慣性地默認卻從不明說的前提。你會更認真地思考：怎樣定義一個概念才是最干凈的？因為在 Lean 中，定義一個概念之后若想使用它，首先需要圍繞這個概念建立一系列基本引理，也就是所謂的 API。

這些引理在論文中往往一筆帶過，“顯然這個概念是單調的”“顯然它在并集下封閉”，但你確實應該證明它們。而如果定義方式不夠恰當，形式化這些“顯然”的陳述會花費兩倍甚至五倍的時間。這種經歷讓我對如何改進自己的寫作有了新的視角。坦白說，有時候我甚至會對合作者產生些許不滿，因為他們還沒有接觸過這種思維方式，仍在沿用舊的非形式化風格。

Heather Macbeth 曾撰文討論形式化和自動化如何催生一種新的證明寫作風格。傳統證明通常是線性的，從 A 推導到 B，你試圖找到一條等式鏈或推理路徑。但借助自動化工具，你可以換一種方式表達：這里有 10 個相關事實，要從 A 到達 B，可以用標準工具找出這些事實的恰當組合來完成任務。這個組合過程往往是技術性的、不太有趣的，比如某種線性代數運算之類。這是一種不同的證明風格，在某種意義上反而更易于閱讀。對人類來說雖然更難手工驗證，但你能更清晰地看到證明的輸入和輸出，而傳統寫法往往把這些信息隱藏了起來。

Peter Scholze 的經歷也印證了這一點，他說過，形式化過程中獲得的反饋實際上幫助他更清晰地思考了那個關鍵引理的具體細節，他認為是非常有益的智識活動。

問：你提出過一個廣為流傳的框架：數學學習的“前嚴謹、嚴謹、后嚴謹”三個階段。這個框架如何與我們正在討論的話題相關聯？

陶哲軒：是的，我寫了那篇傳播甚廣的文章，討論學習數學的三個階段。第一階段是“前嚴謹”階段：你還不真正理解什么是證明，但對什么可行、什么不可行有一些模糊的直覺。這大致是小學階段的數學理解水平，有時直覺是對的，有時是錯的，而你缺乏區分兩者的能力。

第二階段是“嚴謹”階段：你被要求嚴格按照規范行事，每一步都必須正確無誤。在這個階段，人們往往會暫時失去直覺，因為全部注意力都集中在確保每個步驟完全正確上。但這個過程會幫助你清除所有錯誤的直覺，你能看到論證失敗的精確反例，同時保留那些經受住嚴謹檢驗的好直覺。

第三階段是“后嚴謹”階段：你可以在形式化與非形式化之間自如切換。你能夠用非形式化的方式論證，但現在是安全的，因為錯誤的直覺已被清除；而且你知道，必要時可以將其轉換回嚴謹形式。反過來，你也能閱讀一個嚴謹的論證，并將其翻譯成直覺性的語言。

Lean 確實幫助我清理了直覺中一些錯誤或低效的思維模式。一個典型的低效習慣是：在教科書中陳述定理時，我們往往添加過多的假設。出于謹慎，為確保定理正確，我們會堆砌各種額外條件，集合非空、函數連續、參數為正等等。

理想情況下，我們應該對這些假設進行壓力測試。而 Lean 提供的自動檢查器恰好能做到這一點：當你形式化某個證明后，它會提示你“順便說一句，你從未使用過這些假設”，有時這會帶來真正的進展。人們可能長期存在某種思維定勢，認為某個工具只能在特定條件下使用，但證明本身其實并不依賴那個條件，只是從未有人注意到。形式化讓我們能夠自動發現每個工具的自然適用范圍，這非常有價值。

問：這個總結非常精到。我們一直在思考的一個問題是：軟件工程和計算機科學中的深層洞見如何影響人們對數學認知和數學研究的理解。你之前提到形式化如何清晰化每個定理的假設和輸出，本質上就是良好的軟件工程實踐。Dijkstra 有一整套關于前置條件和后置條件推理的理論；同樣，隨意傳播各種可能的假設是軟件工程中典型的反模式。

我特別想問的是：你在形式化過程中的“頓悟時刻”是什么？學習一門小眾的學術編程語言顯然需要跨越最初的門檻，但在什么時刻你意識到，將數學轉化為軟件的過程本身也能加速理解，甚至推動數學發現？對我而言，這個時刻出現在形式化連續統假設獨立性證明的過程中：我陷入困境，所有源材料都存在問題，然后我發現可以通過開關某些關鍵假設，迅速獲得比任何教科書都更深刻的理解。我好奇你有怎樣的類似經歷。

陶哲軒：有兩個時刻給我留下了深刻印象。

第一個發生在形式化 PFR 猜想的證明時。這是加性組合學中的多項式 Freiman-Ruzsa 猜想。證明中有一個指數 C，最終等于 12，這是將證明各處的小常數組合起來得到的結果。我們花了三周時間寫出藍圖，動員了 20 個人來形式化這個 C＝12 的證明，全部手工完成，那是在 AI 時代之前。后來有人在 arXiv 上發布了一篇短文，指出如果對源論文做 5 處修改，可以將 12 降到 11。有人問：我們要不要也形式化這個？我心想，形式化 C＝12 花了三周，C＝11 豈不是又要三周？

但實際情況是：你只需在 Lean 的最終陳述中將 12 改成 11，然后觀察哪些代碼行變紅，它們不再被證明正當。你對照新的預印本，發現可以這樣修復這 5 行使其編譯通過；但修復之后，另外 10 行又變紅了；于是你繼續處理那些。一天之內，我們就完成了整個證明向 C＝11 的更新。形式化第一個結果確實繁瑣，但一旦需要修改證明，它的效率遠超傳統方式，即便沒有 AI。

第二個經歷來自另一個項目“等式理論計劃”。有人在形式化他人撰寫的證明時在某一步卡住了，說：“我不知道怎么處理這一步。”我查看了那一行代碼。雖然不理解整個證明，但我能理解那一行及其足夠的上下文，于是告訴他：“你只需要這樣修改這一行，就能使用那個工具了。”我可以給出非常原子化的診斷——如何修復一個 1,000 行代碼中的問題，只需檢查其中 3 行。

這是 Lean 的獨特之處：形式化驗證過的軟件具有高度模塊化的特性，其他軟件難以企及。你可以進行真正原子化的討論，只聚焦于代碼中非常具體的幾行，而無需理解其他部分發生了什么。

在傳統數學中，這種交流只能與那些我完全熟悉的合作者進行。我們必須長期共事，達到能夠理解彼此思維方式的精細程度，甚至能夠接續對方的話。進入那種狀態是美妙的，但我只與少數幾位合作者建立了這樣的默契。與新人合作時，你必須解釋所有定義，還會產生各種誤解。但有了 Lean，這一切障礙都消失了，因為你擁有對問題本質和解決方案的精確類型描述。

它以一種前所未有的方式將數學原子化了。

問：你是互聯網數學協作的先驅之一，包括 Polymath 項目這種眾包數學研究的模式。能否談談你對數學協作的理解在過去 20 年間是如何演變的？以及在這種高度模塊化、有時甚至匿名的互動方式下，數學的未來會呈現怎樣的面貌？另外，你幾年前在 Notices of the AMS 上發表的文章中討論了數學家角色的演變。我好奇，隨著你組織這些形式化項目，你對自身角色的理解發生了怎樣的變化，以及運營 Polymath 項目積累的經驗如何與此相互作用？

陶哲軒：我一直感到想做的數學遠超個人所能完成的范圍，因此始終認為協作極具價值。我從合作者那里學到了很多，也從互聯網上的隨機交流中獲益匪淺。我開始寫博客源于一次偶然經歷：有一次我在個人網頁上發布了一個數學問題，并不指望有人回應。但那時已經有足夠多的人關注我的頁面，三天之內我就收到了關于這個問題來源的完整文獻索引。現在這其實是一個簡單的 ChatGPT 查詢就能解決的問題，但在當時，這對我是革命性的。

后來 Tim Gowers 發起了 Polymath 項目，嘗試眾包數學研究，我非常投入。這與我的理念產生了共鳴。參與者越多，就越有可能產生那種任何單個專家都無法獨自發現的意外聯系。但這些項目始終存在瓶頸：當有一二十人貢獻時，必須有人檢查所有答案、確保整體連貫并撰寫總結。這個人要么是我，要么是 Tim Gowers，要么是其他核心成員。這極其消耗精力，你就像星形網絡的中心節點。

因此，雖然前景誘人，這種范式終究無法規模化。它確實促成了一些非常廣泛的項目，參與者從數學的各個領域貢獻聯系，這些領域與項目的關聯性是組織者事先完全沒有預料到的。但我們缺乏驗證的組織基礎設施。而且當時我們是在博客或 wiki 上運營，而非像現在這樣使用 GitHub。

形式化和 AI 真正實現的，是讓具有不同技能組合的人能夠無縫協作。在形式化項目中，并非每個人都需要精通 Lean，并非每個人都需要深諳數學，也并非每個人都需要熟悉 GitHub。你只需要一組具有重疊技能的人，每個人掌握其中一部分即可。這使得數學項目中真正的分工成為可能。

在傳統數學項目中，你可能有一兩位合作者，但即便是協作，每個人也必須承擔所有工作：每個人都得理解數學、都得會寫 LaTeX、都得能檢查論證，每個環節每個人都要參與。而在真正的分工體系中，有專人管理項目、有專人負責質量保證，就像工業化生產和專業化分工那樣。

軟件工程早已想通了這一點。軟件開發過去也是單槍匹馬的黑客模式，但那種方式無法支撐大規模系統。企業級軟件需要專精于不同領域的人協同工作。我預見數學研究也將越來越多地采用這種規模化、專業化的模式。當然，傳統的手工藝式數學仍將存在并受到珍視，但我們將擁有這種高度互補的新方式。

問：這是否意味著你預見大多數職業數學家的角色將演變為這類工業化系統的架構師？

陶哲軒：我認為“數學家”的定義本身將會拓寬。會有擅長運營大型項目的人，他們是項目經理，懂得足夠的數學和足夠的 Lean 來把握高層面的進展，但未必能解決具體的技術細節；他們的核心能力在于協調大型項目。

會有一些人特別擅長形式化，或特別擅長使用新的 AI 工具，但未必是某個數學分支的領域專家。

人們可以更靈活地加入和離開項目。當然，你也可以選擇更傳統的方式，讓小團隊里每個人深度參與所有環節。我認為這仍然是做數學的重要方式之一。

關鍵在于我們有了選擇。目前，許多熱愛數學的人被排斥在數學研究之外，因為門檻太高了。如果你想參與前沿研究，你需要具備博士級別的數學素養，需要熟練使用 LaTeX，還需要確保寫作不出任何差錯。這對許多數學愛好者來說過于艱巨。而那些確實嘗試參與的人，常常被當作民科打發，因為他們的技能組合存在太多缺口。但社會上確實存在強烈的需求：數學界需要類似“公民科學”的模式。

我現在深度參與一個叫做“Erd?s 問題”的網站，它已經發展成一個社區，幾十位不同數學教育背景的人在貢獻各種工作。我們找到了模塊化問題的方法：也許你無法解決整個問題，但你可以挖掘相關文獻、建立與某個整數序列的聯系、評論他人的證明、進行數值實驗。有一批潛在的人渴望參與研究級別的數學，這些工具有望為他們打開大門。

圖丨Erd?s 問題網站（來源：Erd?s Problem）

問：到目前為止，我們討論了你在形式化前沿的經驗，以及協調大規模數學研究的經驗。我想這是一個合適的時機來談談你正在推動的解析數論邊界形式化項目。也許我們可以從一個簡要說明開始，讓普通讀者理解為什么這個問題重要，以及它如何體現我們之前討論的這些主題？

陶哲軒：讓我提供一個思考框架。我傾向于將自動化視為人類思維的補充工具。使用計算機研究數學，最顯而易見的方式是拿人類想攻克的最難問題，比如黎曼假設，讓計算機去嘗試。計算機在這類人類關注的問題上會取得一定進展，但我認為，至少在近期，它們在那些與人類偏好完全正交的方向上會更加成功。具體而言，那些涉及大量繁瑣數值運算、需要篩選海量排列組合的工作，人類可能不喜歡做，而 AI 完全沒有這種障礙。

在我所研究的方向之一的數論領域，有一個分支包含大量這類繁瑣的計算工作，而迄今為止只有人類能完成。據我估計，思考一個解析數論問題時，至少 70% 的時間消耗在這種苦力活上。

我們擁有許多精妙的想法和工具，可以將一類關于數字、指數和或黎曼 zeta 函數的陳述轉化為另一類我們關心的陳述。但這些工具都有各自的輸入輸出要求，你需要將它們恰當地串聯起來。你可以在論文中找到這些工具，但每篇論文使用不同的符號體系，有時它們的假設條件與你的需求不完全匹配，于是你不得不拆解原始證明，構建自己的版本。

這涉及大量重復造輪子和參數調整的工作，而且容易出錯。為了減輕痛苦，我們發明了一些變通方法。其中之一是聲稱“不關心常數”：與其寫出“這里是常數 27，那里是常數 38”，我們統一用 C 表示，只說“這是某個常數”，不去計算具體數值。這減少了計算量，也在一定程度上防止錯誤。如果你在常數上犯了算術錯誤，但結論仍然表述為“存在常數 C 使得 ……”，就不會造成嚴重后果。

但代價是：我們數論中的許多結果不是顯式的。你可能證明了“每個足夠大的奇數都是三個素數之和”，但“足夠大”究竟是多大？大于某個 C，而這個 C 具體是多少，我沒有算，太麻煩了。

因此，只有一小部分被稱為“顯式數論”的領域會精確計算所有常數。這類工作更加繁瑣，愿意從事的人更少，相關論文讀起來也不愉快，這不是作者的問題，而是內容本身的性質決定的，大量顯式計算本就不具有文學性。

但我認為這恰恰是自動化的理想目標。如果我們能建立某種流水線，將這些顯式論文形式化，其中的核心思想和輸入已經相當清晰，主要挑戰在于匹配眾多略有差異的工具、對齊所有參數，我相信這完全在當前技術的能力范圍之內。在此基礎上，我們還可以利用 AI 或機器學習來尋找最優的串聯方式。

這將為審視整個領域創造全新的視角。例如，如果有人證明了關于黎曼 zeta 函數的新邊界，我們希望能將其“投入”一個包含 100 個形式化定理的庫中，像 Excel 表格一樣自動更新：改變一個單元格，所有相關單元格隨之刷新。

我們可以擁有一個動態的、實時更新的領域知識庫，而非那些寫死指數的靜態論文。目前，每當某個結果改進，就需要手工重寫現有論文來計算最新邊界。對于任何給定的結果，這種更新大約每 10 年才進行一次。但如果有了正確的工具，這可以在幾分鐘內完成。

問：你是說這本質上是一個軟件問題。這或許類似于早期程序員看待匯編語言的方式——繁瑣，子程序隱藏在代碼中，稱不上文學，但一旦能夠在更高抽象層次上推理 ……

陶哲軒：正是如此。現代軟件原則上是可互操作的：你可以調用其他模塊，有標準化的接口讓軟件工具相互通信，你可以構建大規模的復雜生態系統。當然，也因此會有更多 bug。但有了 Lean，我們有望以一種無 bug 的方式實現大量研究者之間的互操作。這是目前根本不存在的東西。

問：你認為數論或其他領域有多大比例的工作是由這類繁瑣活動構成的？

陶哲軒：這個比例很難精確量化，而且我認為影響是間接的。正因為存在這些繁瑣的計算，我們實際上會下意識地調整研究方向來規避它們。當一條思路開始變得計算量巨大、錯綜復雜時，我們往往會繞道而行，轉向其他問題。所以如果只看論文中呈現的內容，繁瑣工作的比例似乎并不高，但那是因為我們一直在繞開路上的坑洞。真正的代價不在于“我們花了多少時間做苦力”，而在于“我們因為不想做苦力而錯過了多少機會”。

我相信當這些工具成熟之后，我們將改變做數學的方式。遇到大規模計算，我們會直接用技術工具去攻克它，而不是繞路回避。我們將能夠突破那些現在幾乎是本能般回避的障礙。所以表面的百分比看起來不高，但如果從錯失機會的角度衡量，代價是巨大的。

問：你之前提到一個主要瓶頸是找到合適的合作者并與他們充分交流、共享思維狀態。就目前人們研究顯式解析數論邊界的方式而言，有多大比例的時間被困在溝通結果、或在人類專家之間進行這種“分布式計算”以傳播邊界？如果你的愿景實現，該領域的研究可以加速多少倍？

陶哲軒：首先存在信任問題。這類計算中，如果某處出現一個錯誤步驟，整個計算就作廢了。所以你必須知道誰是可靠的作者、誰不是。這是隱性信息，我們不會發布“不可靠作者名單”。因此，你必須了解這個社區，知道該向誰請教。如果某個結果不完全在文獻中，但你可以問某位專家，對方會告訴你“對，只需要這樣修改就行”。這里的瓶頸在于：你必須身處這個圈子，認識所有關鍵人物，才能在這個領域有效地工作。

我認為一旦有了形式化帶來的信任保障，這個領域就可以更大程度地開放。你可以使用素未謀面者的結果，只要它經過 Lean 驗證。這將解除大量工作的阻塞。

問：你提到了信任這個概念。一個研究者在某個領域持續工作，隨著時間推移積累聲譽和信任。一個真正激發我對形式化和數學基礎興趣的故事是沃沃斯基（Vladimir Voevodsky）的經歷。他建立了非凡的聲譽，證明了一系列驚人的結果，但在 90 年代末發表的一篇論文中，他大約 10 年后才發現存在一個關鍵錯誤。他由此認識到，所有人信任他只是因為他有輝煌的 track record，但這并不能真正保證正確性。

圖丨沃沃斯基（來源：WikiPedia）

陶哲軒：正是由于這種不斷累積的信任網絡存在局限，目前我們能夠推進數學的深度是有上限的。在分析學中，這個問題相對不那么嚴重，因為我們的構建方式更加貼近基本原理，更接近第一性原理推導。但它確實是數學整體面臨的一個制約因素。

問：作為后續問題：隨著這個項目推進——從羅瑟（Rosser）和施恩菲爾德（Schoenfeld）等人 1960 年代以來的經典論文開始形式化——你認為現有文獻中可能存在多少尚未被發現的錯誤？而這些錯誤中又有多少只是無關緊要的小問題，數學這一學科的整體知識庫對它們是具有魯棒性的？

陶哲軒：我很想知道實際的錯誤率是多少。也許結果會讓我們欣慰，也許會令人不安。6 個月后再問我這個問題吧，屆時我們會找到答案。

參考資料：

https://www.youtube.com/watch?v=4ykbHwZQ8iU

運營/排版：何晨龍