陶哲軒：AI讓數學進入「工業化」時代，數學家也可以是「包工頭」

文章轉載自公眾號“機器之心”

編輯｜張倩、陳陳

很多人提到數學研究，腦子里浮現的還是那個畫面：一個人，一塊白板，來回踱步，等靈感突然降臨。

但當今世界最偉大的數學家之一、菲爾茲獎得主陶哲軒卻告訴我們：這種「手工業時代」的數學研究模式正處于崩潰邊緣，一場由 AI 和形式化證明語言（如 Lean）引領的「工業革命」已經悄然開啟。

這一洞察來自陶哲軒最近的一次訪談：

▲視頻標題：Terry Tao on the future of mathematics

視頻鏈接：

在訪談中，陶哲軒指出，數學研究中存在大量的重復性勞動，如查閱文獻、調整他人論文中的參數以及繁瑣的計算。通過 LLM 輔助的自動形式化（Auto-formalization），這些瑣碎的工作正逐漸變得輕松。

與此同時，Lean 等形式化證明語言與 AI 的深度融合正在改變數學協作的本質。形式化并不只是「把證明寫得更嚴格」，而是把數學拆成了可以獨立驗證的原子步驟。這種原子化讓分布式科研第一次變得可行。

陶哲軒預見到，數學界將出現類似軟件工程的分工模式。未來的數學家可能扮演「架構師」或項目經理的角色，領導大型協作項目。這種模塊化的研究方式可能允許「公民數學家」（非專業領域專家但具備某些技能的人）參與到前沿研究中，降低進入門檻。如此一來，數學研究的進展或顯著加速。

參與訪談的另外兩位數學家分別是前 OpenAI 研究科學家、Morph Labs 創始人 Jesse Han，以及斯坦福大學助理教授 Jared Duker Lichtman。

以下是機器之心整理的訪談記錄。

從幾十年到 18 個月

數學研究正被加速

陶哲軒： 說實話，在我整個學術生涯中，我一直覺得我們做數學的方式少了點什么。我們在研究一個數學問題時，總想找到那個能打開問題大門的精妙想法。但在那之前，有大量枯燥的苦力活。比如文獻綜述，比如你在別人論文里看到一個技巧想用到自己的問題上，但所有的輸入條件都有點不一樣，你就得手動調整所有的論證。還有那些計算 —— 它們確實有用，能幫你建立直覺，但很多時候就是硬磨，不停地算啊算。我以前也試過寫一些小程序來加速某些計算，但那時候技術還不成熟。

大概兩年前，就在 IPAM（純粹與應用數學研究所）這里，我們辦了一個機器輔助證明的會議，我是組織者之一。在那次會議上，我們接觸到了各種各樣的嘗試 ——SAT 求解器、計算機輔助軟件包、大語言模型。ChatGPT 剛問世，還有 Lean。那是一個令人興奮的世界，你突然發現很多事情變得可能了，而且正在發生。比如 Peter Scholze 剛完成了一個長達 18 個月的項目，把他的一個重要定理形式化了 ——

Jared Duker Lichtman：液態張量實驗。

陶哲軒： 對，液態張量實驗。這是個大工程，一個定理花了 18 個月。但這已經被認為是巨大的突破了，因為 20 世紀的那些形式化項目，動輒要花幾十年才能完成。所以這本身就是一個巨大的提速，部分原因是我們已經學會了如何使用軟件工程的那些工具，比如 GitHub，以及更智能地組織這些項目。從那以后，我對 AI 和形式化都產生了濃厚的興趣 ——

Jared Duker Lichtman： 就是因為那次會議。

陶哲軒： 對，沒錯。我開始相信這就是數學的未來，也開始接受一些采訪談這個話題。但到了某個時候，你不能光說不練，得真正動手。所以我就去學了 Lean，花了大概一個月，但其實挺好玩的。這讓我想起了寫本科分析教材的經歷 —— 真的是從基礎開始，把每一步都做到完全嚴格。感覺就像在玩電子游戲。我記得 Kevin Buzzard 說過，Lean 是世界上最好玩的電子游戲，大概是這個意思。

Jared Duker Lichtman： 讓人完全上癮。

陶哲軒： 對某類人來說確實非常上癮。而在過去一年里，大語言模型追上來了，它們現在可以自動形式化單個證明步驟，真正開始減輕形式化過程中的苦力活，甚至到了可以實時完成的程度。這打開了無數的可能性。

形式化正在改變數學思維

把含混經驗轉化為可檢驗的結構

Jesse Han： 我第一次接觸 Kevin Buzzard，是 2017 年他在 MSRI（美國數學科學研究所）教自守形式那門課的時候。幾年后我跟他聊天，他說他當時根本沒在關注那門課的內容，因為那個夏天他正在自學 Lean—— 在 Tom Hales 在第一屆大型證明會議上告訴大家 Lean 將是未來之后。

我自己在第一次學習形式化證明的時候，有一個體會是：我慢慢意識到，其實我從來沒有真正學會清晰地思考數學論證。高等數學的證明里有一種普遍的，或者說文化性的混亂感。我很好奇，當你越來越深入地去預判如何形式化證明時，你對自己數學思維的認知有什么變化？

陶哲軒： 確實有一些變化，改變了我寫論文的方式。我現在能看到那些「隱形假設」—— 那些我們習慣性地默認成立的東西。你會更認真地思考：怎樣才是最干凈的定義方式？因為在 Lean 里，當你定義一個概念并想使用它時，你必須先建立一堆瑣碎的引理，就是所謂的 API，圍繞著每個概念。這些東西在論文里往往是「顯然這個概念是單調的」「顯然它在某種運算下封閉」，但你其實應該證明它們。而且你會發現，如果定義得不夠好，形式化這些「瑣碎」命題要花兩倍甚至五倍的時間。所以這讓我學會了如何精簡自己的寫作。有時候我會對合作者有點不耐煩，因為有些人沒有這個視角，還在用老式的非形式化風格寫東西。

Heather Macbeth 寫過一篇文章，講形式化和自動化如何催生了一種新的證明寫作風格。傳統的證明通常是線性的，從 A 到 B，一步一步推，比如一串等式。但有了自動化工具，你可以說：這里有 10 個相關的事實，用一個標準工具來找出這 10 個事實的正確組合就能完成證明。而這個組合往往很無聊，沒什么意思 —— 你知道某種線性代數之類的東西能從這些事實得出結論。這是一種不同的證明寫作風格，某種意義上反而更容易讀懂。對人類來說更難驗證，但你能更清楚地看到一個證明的輸入和輸出，而傳統寫法往往把這些藏起來了。

Jared Duker Lichtman：Peter Scholze 的情況也是這樣，他說過，在形式化過程中獲得反饋，實際上讓他對某個關鍵引理的細節思考得更清楚了，他覺得這是一個非常有價值的過程。你有一個很棒的框架 —— 前嚴謹階段、嚴謹階段、后嚴謹階段。這個框架怎么融入我們現在討論的話題？

陶哲軒：對，我寫過一篇傳播很廣的文章，講學習數學的三個階段。第一個是前嚴謹階段，你并不真正知道什么是證明，但對什么行得通、什么行不通有一些模糊的直覺。這通常是小學階段對數學的理解方式。有時候你的直覺是對的，有時候是錯的，但你沒有辦法分辨哪個是哪個。

然后是嚴謹階段，你被迫完全按照規矩來，每一步都要做得準確無誤。但在這個階段，你往往會失去直覺，因為你全部的注意力都在確保每一步都正確。不過這有助于清除你所有錯誤的直覺，因為你能看到精確的反例，知道論證在哪里失敗了。而所有好的直覺 —— 那些與嚴謹推理一致的 —— 都會保留下來。

然后是后嚴謹階段，你可以在兩種模式之間自由切換。你可以非形式化地論證，但現在是安全的，因為你已經清除了所有錯誤的直覺。你知道如果需要的話，可以把它轉換回嚴謹的形式。反過來，你也可以讀一個嚴謹的論證，然后把它轉換成直覺性的語言。

Lean 確實幫我清理了一些思維中低效或錯誤的習慣。一個很常見的低效問題是：當你在教科書里陳述一個定理時，往往會加入太多假設。你有點過于保守，想確保證明是對的，就加了一堆額外條件 —— 這個非空、那個連續、這個為正之類的。

Jared Duker Lichtman：你會想去對這些假設進行壓力測試。

陶哲軒：對。但其實還有自動化的 linter 工具，當你在 Lean 里形式化某個東西，證明結束后它會說：「順便提一下，你從來沒用過這個假設。」然后你就會想：「哦，確實，我其實根本不需要正性條件。」文獻里確實有過這樣的真正突破：人們心里有個思維定式，覺得某個工具只能用在比如正數的情況下，但其實證明在沒有正性條件的情況下照樣成立，只是沒人注意到。形式化能讓你自動發現每個工具的自然適用范圍。這已經非常有用了。

Jesse Han：這個說法很精辟。我們花了很多時間思考一個問題：來自軟件工程和計算機科學的深度洞見，如何影響人們對數學認知和數學研究的思考方式。你剛才說的形式化如何讓我們更清楚地理解每個定理的假設和輸出，這其實就是良好的軟件工程實踐。Dijkstra 就專門講過，人們應該更多地去推理前置條件和后置條件。同樣的道理，數學家習慣在定理里堆一堆可能用不上的假設，這在軟件工程里是典型的反模式 —— 一種公認的壞習慣。

兩個頓悟時刻

形式化正在改變數學領域協作方式

Jesse Han：我特別想問你的是：你在形式化過程中的「頓悟時刻」是什么？顯然一開始有很高的啟動門檻，你得學習所有這些關于這門小眾學術編程語言的晦澀知識。但是，在哪個時刻你意識到，把數學變成軟件這個過程，不僅僅是翻譯，還能加速你的理解，加速數學發現的過程？

對我來說，是在形式化連續統假設的獨立性時。有一個時刻我完全迷失了，所有的參考資料都是錯的，但我發現可以打開或關閉某些關鍵假設，然后很快就獲得了比任何教科書都深得多的理解。我很好奇你有沒有類似的經歷。

陶哲軒：有，我有兩個印象特別深刻的時刻。

第一個是我在形式化一個和合作者一起證明的定理，叫 PFR 猜想 —— 多項式 Freiman-Ruzsa 猜想。結論里有一個指數常數，我們當時證明的是：存在一個常數，使得某個性質成立，而這個常數最后算出來是 12。原因并不神秘，只是把證明中所有零零碎碎的小常數一路累積下來，最后自然就變成了 12。

我們花了大概三周時間，把這個「C 等于 12」的結論完整形式化成 Lean 代碼。那是一個完全沒有 AI 的年代，整整 20 個人，全靠手工，是一次非常浩大的工程。

后來，有人往 arXiv 上放了一個很短的預印本，說如果你回到原始論文，只要做五個小改動，就可以把這個 12 降到 11。于是大家就開始討論：那我們要不要把 C 等于 11 也形式化一遍？問題在于，C 等于 12 已經花了我們三周時間，那再來一遍豈不是又是三周？

實際情況并不完全是這樣，但直覺上你幾乎只是把最終定理里的 12 改成 11。然后你會發現，大概有五行代碼變紅了，也就是證明不再成立了。但你去看那篇新的預印本，就會發現，哦，這五行我知道該怎么改。結果一改，這五行是好了，又有另外十行變紅了。于是你再回去改那十行。就這樣來回幾次，我們在一天之內就把整個證明更新成了 C 等于 11。

所以，形式化確實很繁瑣，尤其是第一次把一個結果完整寫出來的時候。但一旦你想修改一個已有的證明，它就比傳統數學方式好得多。這是我第一個非常深刻的體會。

第二個經歷來自一個名為 Equation of Theories 的項目，然后對一項研究進行形式化時，有一次很深的體會。當時有人在把另一位作者寫的證明形式化，結果卡在了某一步。我當時也并不了解整個證明的全貌，甚至可以說完全不理解整體結構，但我盯著那一行代碼看了一會兒，發現我其實能理解這一行在做什么。

我能夠理解足夠多的上下文，從而指出：你這里其實只需要復制并稍微修改這一行，讓它在類型上匹配，這樣就能調用這個工具了。

也就是說，我只通過檢查一千多行代碼中的三行，就給出了一個非常原子級（atomic）的診斷，精確地指出了這個證明該如何修復。

我認為這正是 Lean，乃至形式化驗證軟件的一大特點：它具有一種高度模塊化的結構，這是很多其他軟件甚至傳統數學中并不具備的。你可以圍繞某一行、某一個非常具體的局部問題展開極其精細的討論，而完全不需要理解系統的其余部分。

而在傳統數學中，只有在與你長期合作、彼此已經在思維方式上高度對齊的情況下，才能做到這一點。那種狀態下，你們幾乎可以在極其細微的層面上互相理解，甚至補全對方的句子。

通常情況下，當你和一個尚未在思維方式上充分同步的人討論數學問題時，是很難進行這種粒度如此之細的交流的。

所以你確實可以進入那種高度專注、默契協作的狀態，那種感覺非常好。但現實是，能讓我進入這種狀態的合作者其實只有少數。更多時候，合作中充滿了翻譯成本：你需要反復澄清定義、解釋背景，也不可避免地會出現各種誤解。

而在 Lean 中，這些問題在很大程度上都會消失。因為你面對的是一個對問題和修復方式都有著精確定義的類型描述。問題是什么、哪里不匹配、該如何修復，都被明確地寫進了系統里。Lean 以一種此前從未有過的方式，把數學原子化了 —— 這是其他做數學的方法所不具備的。

數學進入「工業化」時代

數學家也可以是架構師

Jared Duker Lichtman：順著這個話題再往前想，其實也很有意思：我們正在用一種全新的方式來使用數學。你經歷過互聯網的興起，也算是較早參與并推動了類似 Polymath （博學者項目）這種協作式研究項目的人之一。也許你可以談談，你對協作的直覺是如何形成的？在過去大約二十年的時間里，這種協作方式是如何演化的？

以及展望未來，在一種高度模塊化的交互模式下，有時甚至是匿名的協作中，數學研究可能會呈現出怎樣的新形態？

Jesse Han：我想再補充一點。你在幾年前發表于《Notices of the American Mathematical Society》的一篇文章里，提到過一個非常有意思的觀點：你如何看待數學家角色的演變。

我也很想聽你進一步展開這一點，因為這和我們剛才討論的內容高度相關，比如，當你開始主導、協調這些形式化項目時，你是否也感受到自己角色的變化？以及你在組織 Polymath 項目過程中積累的經驗，又是如何與這種變化發生交匯、相互影響的？

陶哲軒：我一直都有一種很強烈的感覺：我想做的數學，遠遠超過了一個人所能完成的量。因此，我始終覺得合作極其高效、也極其重要。我從合著者身上學到了很多，同樣也從互聯網上一些看似偶然的交流中學到了很多。

舉個例子，我最早開始寫博客，其實源于一次非常偶然的經歷。有一次，我在自己的網頁上隨手貼了一個數學問題，并沒有期待會有人回應。但當時已經有不少人會瀏覽我的頁面，結果在短短三天之內，就有人給了我一個非常完整的參考說明，直接指出這個問題最早的來源。放在今天，這可能只需要一次簡單的 ChatGPT 查詢就能得到答案，但在當時，這對我來說是一種顛覆性的體驗。

后來，英國數學家 Timothy Gowers 提出了 Polymath 項目，希望通過眾包的方式來做數學研究，而我也非常享受參與其中。這種想法和我的直覺高度契合：數學中存在著大量潛在的聯系，參與的人越多，就越有可能產生那些偶然的連接，這些連接往往是任何單一專家、無論多么資深，都很難憑一己之力發現的。

但與此同時，這種協作方式始終存在一個明顯的瓶頸。

在 Polymath 項目中，當同時有十幾、二十個人參與貢獻時，總需要有人來逐條檢查這些想法，確保邏輯上一致，并把零散的討論整理成一個連貫、可讀的整體。這個工作通常由我、Timothy Gowers，或者其他少數人來承擔，而這件事實際上是非常耗費精力的。

Jared Duker Lichtman：原本看似去中心化的群體協作，最終還是回到了一個核心人物 + 眾多貢獻者的老模式。

陶哲軒：對，這種模式雖然很有潛力，但并沒有真正實現規模化。不過，它確實促成了一些非常宏大的研究項目：來自數學中完全不同方向的人，會因為偶然的靈感，貢獻出大量有價值的線索。很多時候，項目的組織者事先根本不知道這些人彼此之間存在任何關聯，但他們提供的想法卻是相關且有用的。

問題在于，當時我們并沒有完善的組織與驗證基礎設施。而且那時我們主要是通過博客和 Wiki 來運作項目，而不是像今天這樣使用 GitHub 這類更成熟的協作平臺。

也正是在這里，形式化工具和 AI 展現出了另一項關鍵能力：它們真正實現了不同技能背景人群之間的無縫協作。在一個形式化項目中，并不是每個人都需要懂 Lean，也不是每個人都需要精通數學，更不是每個人都要熟悉 GitHub。你只需要一個技能集合彼此有重疊的群體：每個關鍵環節都有一部分人能夠勝任，整體就能順利推進。

這也使得數學研究第一次真正具備了分工協作的可能性。

在傳統數學研究中，無論是單人還是合作，參與者幾乎都需要什么都懂：既要理解全部數學內容，又要會寫 LaTeX、檢查推導、整理論文，每個人都要覆蓋所有環節。而在真正意義上的分工體系中，就像工業化生產一樣，會有人負責項目管理，有人負責質量驗證，有人專注于具體技術細節。

軟件工程其實早就完成了這種轉變。早期的軟件開發也是一個人包辦一切，但這種方式無法擴展；一旦進入企業級開發，就必須依賴高度專業化的角色分工。

因此，我確實預見到一種趨勢：在規模化、工業化的條件下生產數學成果，并且伴隨著清晰的專業分工。當然，傳統的、手工式的數學研究依然會存在，也依然會被高度珍視；只是未來會出現一種與之互補的、全新的數學生產方式。

Jesse Han：那么，這是否意味著你預見到，大多數職業數學家的角色將會演變為這些工業化數學體系的架構師？

陶哲軒：我認為，數學家的定義本身會被拓寬。未來會出現一類人，他們擅長運作和管理大型項目，就像大型工程中的項目負責人一樣。這些大型項目的管理者會掌握足夠多的數學和 Lean 知識，能夠在宏觀層面理解項目在做什么，但他們未必擅長定位和修復某一條具體的形式化問題。盡管如此，他們能夠協調復雜項目的推進，而這本身就是一種非常重要的能力。

同時，也會有一些人，他們可能并不是某個數學領域的專家，但非常擅長形式化工作，或者非常善于使用新的 AI 工具。這些能力本身同樣有價值。

在這樣的體系中，人們可以更自由地加入或離開項目，協作將變得更加流動。當然，也仍然會存在更傳統的研究方式：由一個規模較小的團隊組成，所有人都深度參與項目的每一個環節。這種方式依然非常重要，也不會消失。關鍵在于，我們終于擁有了多種選擇。

在當前體系下，許多真正熱愛數學的人被擋在數學研究之外，只是因為門檻太高了。如果你想參與前沿研究，就必須掌握博士階段水平的數學；你還得會用 LaTeX；得知道如何寫作、如何避免任何細節錯誤…… 這些要求疊加在一起，對很多人來說極具威懾性，進入門檻過高。

即便成功進入這一體系的人，也常常因為自身技能結構不完整而被忽視或邊緣化。但未來并不必然如此，隨著工具、形式化和協作方式的變化，這種狀況有可能被根本性地改變。

Jared Duker Lichtman：在門檻被工具和協作機制降低之后，數學研究不再只屬于少數職業數學家，而可以像公民科學一樣，吸納大量具有興趣和部分技能的普通參與者。

陶哲軒：是的，我們其實已經在看到這種趨勢了。比如我自己就深度參與過一個數學問題網站。它逐漸發展成了一個社區，聚集了幾十位數學背景和受教育程度各不相同的參與者，大家各自貢獻一些小而具體的內容。

我們學會了把一個問題模塊化拆解：也許你沒法完整地解決這個問題，但你可以幫忙查找相關參考文獻；或者把問題和某個整數序列聯系起來；或者評論、改進他人的證明；又或者做一些數值實驗和計算。

正是通過這種方式，很多人都能在自己能力范圍內參與進來。

而現實中，確實存在著一個非常龐大的群體，他們渴望參與研究級別的數學工作，只是過去缺乏合適的入口和工具。我希望，也相信，這些新的工具和協作方式，能夠真正釋放出這股力量。

AI 應該先幫數學家「干臟活」

Jesse Han：到目前為止，我們已經談了很多內容：一方面是你在形式化數學前沿工作的經驗，另一方面是你在協調大規模協作項目、加速數學研究方面的實踐。而我覺得，正好在這兩者的交匯點上，是一個非常合適的時機，來談談你目前特別投入、也非常興奮推動的一個項目，解析數論中數學界限（Bounds）的形式化證明。

或許我們可以從一個簡要的介紹開始：面向非專業讀者，能否先解釋一下 —— 為什么這個問題本身如此重要？以及它在某種程度上，如何成為我們剛才討論過的那些問題（協作、形式化、規模化研究）的一個縮影或體現？

陶哲軒：我想先從一個更宏觀的角度來講。我一直認為，自動化本質上是對人類思維的補充工具。

最直觀的一種思路是：把人類最想解決、也最困難的數學問題 —— 比如像黎曼猜想這樣的重大猜想，直接交給計算機，讓它們來嘗試解決。計算機在這些問題上確實可能取得一定進展，但我認為，在可預見的未來，它們更有可能在另一類完全不同的任務上發揮巨大優勢。

這些任務往往與人類真正擅長、或樂于從事的工作是正交的，尤其是那些需要進行大量枯燥的數值計算、枚舉海量可能性、反復篩選組合情況的工作。這類任務人類通常并不享受，甚至極易出錯，但對 AI 和計算機來說卻并不構成障礙。

以我所從事的領域之一解析數論為例，這里就存在一個非常典型的困難：其中有大量極其繁瑣、細碎的組合性計算工作，長期以來幾乎只能由人類親自完成，而這正是自動化和 AI 最有潛力介入、并發揮巨大價值的地方。

Jared Duker Lichtman：對我個人來說，在思考一個解析數論問題時，至少有 70% 的時間，都花在這種繁瑣、機械性的工作上。

陶哲軒：是的，我認為我們其實已經掌握了很多非常精巧的思想和工具，可以把關于數字的一類陳述，或者關于和的展開、各種算術函數等內容，轉化為我們真正關心的另一類陳述。解析數論中正是依靠這些工具在不同表述之間來回轉換。

但問題在于，這些工具都有各自的輸入和輸出條件，而真正做研究時，你需要把它們一環一環地串聯起來。相關的工具和結果分散在不同的論文中，每篇論文使用的記號體系都不一樣，假設條件也往往和你手頭的問題并不完全匹配。于是你不得不重新拆解原有證明，根據自己的需求重寫一套版本。

在這個過程中，就會產生大量的重復勞動：反復調整參數、對齊條件、重建推導鏈條，而且非常容易出錯。

為了讓事情稍微不那么痛苦，我們發展出了一些權宜之計。其中一個最常見的做法是：不去關心具體常數。比如這里原本是 27，那里是 38，我們干脆都記成一個統一的常數 C，只說明存在某個常數，而不去計算它的具體數值。這樣可以顯著減少計算量，也能在一定程度上避免錯誤，即便你在常數上算錯了，只要結論仍然成立，通常也不會造成嚴重后果。

但這種做法是有代價的。它導致解析數論中的很多結果都是非顯式的。比如你可能證明了：所有足夠大的奇數都可以表示為三個素數之和，但足夠大究竟是多大？這個常數 C 到底是多少？我們并沒有算出來，說白了，是懶得算。

因此，真正去顯式計算所有常數的解析數論研究，只占整個領域中非常小的一部分。這類工作極其繁瑣、計算量巨大，做的人很少，論文也往往不太好理解。這并不是作者水平的問題，而是因為研究內容本身就充斥著大量細碎、明確的計算過程，幾乎沒有那種直觀的結構美感可言。

說實話，這種研究并不好理解。但我認為，這恰恰是自動化最理想的應用場景之一。如果我們能夠搭建一條流水線，把這些顯式型的論文納入進來，其中的思想和工具本身其實已經相當成熟，真正困難的只是把大量彼此略微不兼容的工具拼接在一起，并把所有參數對齊，那么，用現有的方法就完全有可能在規模化條件下完成這些形式化工作。

在此基礎上，我們甚至可以引入 AI 或機器學習，去探索這些工具鏈的最優組合方式。這將為整個領域打開許多全新的觀察視角。

舉個具體的例子：如果有人在某個算術函數上證明了一個新的界，我們希望能把這個結果直接丟進一個已經形式化好的、包含上百條定理的系統中，然后像操作 Excel 表格一樣自動更新，改動一格，所有依賴它的結果都會自動刷新。

這樣一來，我們就可以擁有一個持續演化、動態更新的領域最前沿狀態，而不再是那些寫死了指數和常數的論文。現在的做法是：每當某個關鍵結果被改進，研究者往往需要重寫整篇論文，重新推導所有相關界限，才能弄清楚最新的最好結果是什么。而這類更新，通常十年才發生一次；但如果工具鏈足夠成熟，這些工作完全可以在幾分鐘內完成。

Jesse Han：所以你的意思是，這本質上是一個軟件問題，對嗎？就像早期編程時代，人們看待匯編語言時那樣，它非常繁瑣，到處都是子程序，邏輯隱藏在代碼細節里，既不直觀，也談不上可讀性。但一旦能夠在更高層次上對這些內容進行抽象和推理，情況就會完全不同。

陶哲軒：可以這么理解。而且在現代軟件工程中，原則上一切都是可以互操作的。你可以調用別人的子程序，不同工具之間有標準化的接口和格式，它們能夠彼此通信，從而構建起極其復雜、龐大的軟件生態系統。

當然，這樣的系統也會帶來一個問題：正是因為系統復雜、組件眾多，軟件中不可避免會出現各種錯誤。

但在數學形式化這件事上，像 Lean 這樣的工具，至少在理論上，讓我們有機會構建一種盡可能無 bug 的協作體系。通過形式化驗證，你可以希望、甚至確信這些由大量研究者共同構建的成果是相互兼容、邏輯一致的。而這正是我們目前在數學研究中所缺失的東西：一種真正可靠、可互操作、可規模化擴展的基礎設施。

當新工具出現

數學的研究路徑會整體改寫嗎？

Jared Duker Lichtman：那么你是否愿意做一個大致的判斷或推測：在數論，乃至其他數學領域中，有多大比例的工作其實是由這些相對枯燥、機械性的勞動構成的？如果這種工作負擔的比例發生改變，是否可能由此催生一種截然不同的研究工作流程？

Jesse Han：我想在這個問題上再補充一句。事實上，在數學史上，應該已經出現過不少并非基于形式化驗證、也不依賴計算機的例子：某些更好的數學技術或方法被發明出來之后，使數學家得以擺脫以往的一些繁瑣勞動，從而能夠把精力投入到全新的問題和思考方式中。

我也很好奇，在解析數論的發展過程中，是否存在過這樣的重要例子？比如，是否有某些關鍵方法的出現，真正改變了人們理解和研究這一領域的方式？

如果是這樣的話，那么我們是否也可以把如今的形式化工具（如 Lean）以及自動形式化技術，視為歷史上這一類技術演進的又一個實例，一次新的數學技術革命？

陶哲軒：我認為數論其實是最早采用實驗性方法的數學分支之一。例如，數論中的一個核心問題，關于素數分布的規律，最早就是由高斯提出的猜想。

高斯當年通過一種極其艱苦的方式來獲得直覺：他手工計算了前幾十萬、甚至上百萬個素數，并從這些數據中觀察到了某些模式，由此提出了后來影響深遠的素數分布猜想。

從今天的角度看，這幾乎就是一種早期的計算實驗數學：通過大量具體數據的積累，來引導理論判斷和猜想的形成。這在當時是非常開創性的做法，也深刻影響了數論此后的發展方向。

Jared Duker Lichtman：而且當時所依賴的，其實只是規模很小的數據。

陶哲軒：是的。高斯展現出了一種非凡的能力：他能夠從規模非常小的數據集中，概括出極其深刻、普遍的規律，這正是高斯天才的體現，也正因為如此，后來很多工具都會以他的名字命名。

而隨著計算技術的發展，我們才真正能夠系統性地展開這種探索。后來也陸續出現了不少類似的例子：一些重要的猜想最初正是通過數值實驗和計算探索被發現的；而在更近的時代，還有一些結果是借助大規模枚舉，甚至結合機器學習方法，才逐漸顯現出其結構和規律的。

這些進展都說明了一點：新的技術手段不斷擴展著數學家可探索的空間，也在持續改變人們理解和研究數論的方式。

Jared Duker Lichtman：我想，甚至連圖靈當年也在做類似的事情，親自去計算函數的零點。

陶哲軒：像某些算術函數的研究，其實早期就大量依賴數值計算。比如黎曼猜想，在很長一段時間里，正是通過大量數值實驗獲得了強有力的支持。

因此，歷史上早就存在這樣的先例：計算機的引入，催生了一種新的數學研究方式，不再只是依賴純粹的抽象思考，而是結合數據和實驗來推動理論的發展。

當然，我們現在討論的這種形式化工作，并不完全等同于數據驅動的數學，但它無疑是一種計算機輔助的研究模式。

Jared Duker Lichtman：那么，撇開機器學習領域里那一小部分人，或者少數主動嘗試新工具的研究者不談，對于一位普通的數學家來說，無論是在數論還是其他領域，在日常研究工作中，有多大比例其實是被這種繁瑣、機械性的苦工所拖慢、所構成瓶頸的？

陶哲軒：這個問題其實很難給出一個精確的百分比，但我覺得關鍵并不在于直接統計時間比例，而在于一種間接影響。

正是因為這些繁瑣勞動的存在，我們往往會有意識地改變做數學的方式，盡量減少自己要面對的苦工。比如，當我們意識到某一步組合推導開始變得非常凌亂、計算量巨大時，往往會選擇刻意繞開，改用另一條思路繼續推進。

因此，如果你只看最終論文里呈現出來的內容，會覺得我們似乎做的都是高判斷力的工作，真正的苦工并不多。但那是因為我們在研究過程中，已經下意識地避開了道路上的一個個坑，用一個比喻來說，我們是在不斷繞開崎嶇路段，而不是去填平它們。

而一旦這些工具真正到位，情況可能會發生根本變化。那時，我們會改變做事方式：如果前方出現一個巨大而繁重的計算任務，我們不再選擇繞路，而是直接碾過去，動用所有可用的技術手段，借助計算、形式化工具，甚至直接交給計算機，說清楚從這里到那里該怎么走，然后繼續前進。

這樣一來，我們就可以穿越那些現在幾乎是下意識回避的障礙。所以，從表面上看，當前數學研究中苦工的比例似乎并不高；但如果把那些被我們主動規避掉的工作也算進去，那這個比例其實遠比看上去要大得多。

Jesse Han：之前你提到過，一個非常重要的瓶頸在于：尋找合適的合作者本身就很困難，更不用說還要在工作方式、思路層面與他們建立足夠的默契。

我想具體問的是：在這種情況下，你覺得在研究過程中，有多大比例的時間，其實是被人與人之間溝通、對齊思路、傳遞和同步這些界限結果所消耗的？也就是說，為了在人類專家之間完成某種分布式計算，我們究竟付出了多大的溝通成本？

以及，如果你所設想的這一愿景真的實現了形式化、自動化工具能夠承擔起這些傳遞與整合工作，你認為這一領域的數學研究整體上有可能被加速多少倍？

陶哲軒：我覺得確實如此。首先，這是一個信任問題。在這類計算密集的研究中，只要某一步出了錯，整個推導就可能全部失效。因此，你必須清楚哪些作者是可靠的、哪些結果是可以放心使用的，而這些信息往往是隱性的，并不會明確寫在論文里。

現實中，我們不會公開列出哪些工作存在嚴重問題，于是你只能依賴對學術共同體的熟悉程度：你得知道這個圈子，知道該去問誰。很多時候，如果某個結果還沒有正式發表，但你認識相關領域的專家，就可以直接去問他：這個地方是不是只需要稍微改一下就行？對方可能就會給你一個可靠的判斷。

這就形成了一個明顯的瓶頸：你必須身處這個關系網絡之中，認識足夠多對的人，才能高效地在這個領域工作。

而一旦我們能夠通過形式化工具（比如 Lean）提供這種可驗證的信任保證，情況就會發生根本改變。那時，你可以放心使用來自陌生研究者的結果，即便你從未見過他們，因為所有證明都已經由系統嚴格驗證過。

正是在這一點上，我認為形式化將會極大地解鎖生產力，消除大量由于信任與溝通成本造成的阻塞，從而釋放出此前被壓抑的大量研究潛力。

Jared Duker Lichtman：是的，我明白你的意思。你剛才提到信任這個概念，其實在數學研究中，信任往往是通過長期積累的學術記錄建立起來的。一個研究者在某個領域持續工作、不斷產出成果，隨著時間推移，其他人自然會越來越信任他的結論。

而真正讓我開始對形式化和數學基礎問題產生強烈興趣的一個重要故事，正是關于一位數學家的經歷。他曾經建立起極高的學術聲譽，證明過許多非常了不起的結果，因此在學界擁有極強的可信度。

但在 20 世紀 90 年代末，他寫過一篇論文，后來大約在十年之后，他才意識到其中存在一個關鍵性的錯誤。回過頭來看，他自己也反思到：當時很多人之所以接受那篇結論，很大程度上是因為大家在相信他這個人，而不是因為證明本身被徹底、逐行地驗證過。

而這正揭示了一個核心問題：個人聲譽和過往記錄，并不等同于真理的保證。這類經歷也正是形式化證明與基礎工具如此重要的原因之一，它們提供的不是基于人的信任，而是基于可驗證結構的信任。

陶哲軒：當然，這種做法在深度上是有極限的。我們能夠推動數學前進的程度，終究會受到限制。當前在分析學中，這個問題相對沒那么嚴重，是因為這里逐漸形成了一張不斷加密的信任之網，而且我們的工作方式往往更接近從第一性原理出發，比其他一些領域更少依賴遠距離的結果。

但即便如此，這種基于信任的結構依然是數學發展的一個限制因素。從長遠來看，這是一個無法回避的問題，也是形式化和基礎工具之所以重要的又一個原因。

Jared Duker Lichtman：我想再追問一個相關的問題。隨著我們開始系統性地回溯并形式化一些經典論文，以及從 20 世紀 60 年代以來的大量文獻，你會如何看待這樣一個問題：

第一，在現有的數學文獻中，可能還存在多少尚未被發現的錯誤？

第二，這些錯誤中，有多少只是可以通過小修小補解決的技術性問題？換句話說，整個數學體系作為一個整體，對這類錯誤究竟有多強的魯棒性？

也就是說，即便我們真的通過形式化手段暴露出大量隱藏的問題，它們是否大多不會動搖理論的核心結構，而只是需要局部修正？還是說，其中也可能存在少量但影響深遠的根本性漏洞？

陶哲軒：說實話，我也很想知道實際的錯誤率到底是多少。也許結果會讓我們驚喜，也可能會讓我們不太愉快。等六個月之后再來問我吧。

Jesse Han：今天這次交流真的非常愉快，真希望能再多聊一會兒。那就希望六個月之后，我們還能再進行一次這樣的對話。