近日，Math Inc. 與知名數(shù)學(xué)家陶哲軒進(jìn)行了一場(chǎng)深入對(duì)話。作為 2006 年菲爾茲獎(jiǎng)得主，他近年來(lái)在形式化數(shù)學(xué)與 AI 輔助證明領(lǐng)域的探索引發(fā)了學(xué)界廣泛關(guān)注。

從 2023 年底領(lǐng)導(dǎo)團(tuán)隊(duì)在三周內(nèi)完成多項(xiàng)式 Freiman-Ruzsa 猜想（Polynomial Freiman-Ruzsa Conjecture，PFR）的 Lean 形式化驗(yàn)證，到 2024 年發(fā)起的“等式理論計(jì)劃”（Equational Theories Project），陶哲軒正在身體力行地推動(dòng)一場(chǎng)數(shù)學(xué)研究范式的變革。這次對(duì)話中，他坦誠(chéng)地分享了自己對(duì)形式化工具、AI 技術(shù)以及數(shù)學(xué)未來(lái)的思考。

（來(lái)源：Youtube）

他的核心觀點(diǎn)包括：

一、形式化正在改變數(shù)學(xué)寫(xiě)作和思維方式。Lean 等工具迫使數(shù)學(xué)家更清晰地定義概念、檢驗(yàn)假設(shè)，能自動(dòng)發(fā)現(xiàn)“你其實(shí)從沒(méi)用過(guò)這個(gè)假設(shè)”——這有時(shí)帶來(lái)真正的數(shù)學(xué)進(jìn)展。

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

三、數(shù)學(xué)研究可以像軟件工程一樣分工協(xié)作。不是每個(gè)人都需要懂 Lean、懂?dāng)?shù)學(xué)、懂 GitHub——只需要重疊的技能組合。這將讓更多“數(shù)學(xué)愛(ài)好者”參與前沿研究。

四、解析數(shù)論是自動(dòng)化的理想目標(biāo)。該領(lǐng)域約 70% 的工作是繁瑣的常數(shù)計(jì)算和參數(shù)匹配，一旦形式化，就能像 Excel 一樣自動(dòng)更新——有人證明了新邊界，整個(gè)領(lǐng)域的相關(guān)結(jié)果可在幾分鐘內(nèi)同步更新。

五、形式化建立了新的信任基礎(chǔ)設(shè)施。傳統(tǒng)數(shù)學(xué)依賴“圈子”和聲譽(yù)來(lái)判斷結(jié)果可靠性；有了 Lean 驗(yàn)證，你可以使用素未謀面者的結(jié)果。

以下是對(duì)話全文。

問(wèn)：你是從什么時(shí)候開(kāi)始對(duì)機(jī)器輔助證明產(chǎn)生興趣的？

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

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

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

圖丨 Peter Scholze（來(lái)源：WikiPedia）

問(wèn)：那次會(huì)議促使你開(kāi)始學(xué)習(xí) Lean？

陶哲軒：那次會(huì)議之后，我對(duì) AI 和形式化都產(chǎn)生了濃厚興趣，并確信這就是數(shù)學(xué)的未來(lái)方向。我開(kāi)始接受采訪，四處談?wù)撨@些想法。但到了某個(gè)節(jié)點(diǎn)，光說(shuō)不練是不行的，必須真正動(dòng)手。于是我開(kāi)始學(xué)習(xí) Lean，大約花了一個(gè)月時(shí)間。這個(gè)過(guò)程其實(shí)相當(dāng)有趣，讓我想起當(dāng)年撰寫(xiě)本科實(shí)分析教材的經(jīng)歷——從自然數(shù)的構(gòu)造講起，把每一個(gè)細(xì)節(jié)都處理得完全嚴(yán)謹(jǐn)。使用 Lean 的感覺(jué)很像在玩電子游戲。Kevin Buzzard 曾說(shuō) Lean 是“世界上最好的電子游戲”，對(duì)某類(lèi)人來(lái)說(shuō)確實(shí)極易上癮。

而在過(guò)去一年里，大語(yǔ)言模型的能力突飛猛進(jìn)，已經(jīng)能夠自動(dòng)形式化單個(gè)證明步驟，大幅減輕了形式化過(guò)程中的繁瑣工作。現(xiàn)在甚至可以實(shí)時(shí)進(jìn)行形式化，這打開(kāi)了無(wú)數(shù)新的可能性。

問(wèn)：我在學(xué)習(xí)形式化證明的過(guò)程中有一個(gè)深刻體會(huì)：我逐漸意識(shí)到自己其實(shí)從未真正學(xué)會(huì)清晰地思考數(shù)學(xué)論證。高等數(shù)學(xué)的證明中似乎存在某種約定俗成的模糊性。隨著你越來(lái)越深入地接觸形式化，你對(duì)自身數(shù)學(xué)認(rèn)知的理解是否也發(fā)生了變化？

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

這些引理在論文中往往一筆帶過(guò)，“顯然這個(gè)概念是單調(diào)的”“顯然它在并集下封閉”，但你確實(shí)應(yīng)該證明它們。而如果定義方式不夠恰當(dāng)，形式化這些“顯然”的陳述會(huì)花費(fèi)兩倍甚至五倍的時(shí)間。這種經(jīng)歷讓我對(duì)如何改進(jìn)自己的寫(xiě)作有了新的視角。坦白說(shuō)，有時(shí)候我甚至?xí)?duì)合作者產(chǎn)生些許不滿，因?yàn)樗麄冞€沒(méi)有接觸過(guò)這種思維方式，仍在沿用舊的非形式化風(fēng)格。

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

Peter Scholze 的經(jīng)歷也印證了這一點(diǎn)，他說(shuō)過(guò)，形式化過(guò)程中獲得的反饋實(shí)際上幫助他更清晰地思考了那個(gè)關(guān)鍵引理的具體細(xì)節(jié)，他認(rèn)為是非常有益的智識(shí)活動(dòng)。

問(wèn)：你提出過(guò)一個(gè)廣為流傳的框架：數(shù)學(xué)學(xué)習(xí)的“前嚴(yán)謹(jǐn)、嚴(yán)謹(jǐn)、后嚴(yán)謹(jǐn)”三個(gè)階段。這個(gè)框架如何與我們正在討論的話題相關(guān)聯(lián)？

陶哲軒：是的，我寫(xiě)了那篇傳播甚廣的文章，討論學(xué)習(xí)數(shù)學(xué)的三個(gè)階段。第一階段是“前嚴(yán)謹(jǐn)”階段：你還不真正理解什么是證明，但對(duì)什么可行、什么不可行有一些模糊的直覺(jué)。這大致是小學(xué)階段的數(shù)學(xué)理解水平，有時(shí)直覺(jué)是對(duì)的，有時(shí)是錯(cuò)的，而你缺乏區(qū)分兩者的能力。

第二階段是“嚴(yán)謹(jǐn)”階段：你被要求嚴(yán)格按照規(guī)范行事，每一步都必須正確無(wú)誤。在這個(gè)階段，人們往往會(huì)暫時(shí)失去直覺(jué)，因?yàn)槿孔⒁饬Χ技性诖_保每個(gè)步驟完全正確上。但這個(gè)過(guò)程會(huì)幫助你清除所有錯(cuò)誤的直覺(jué)，你能看到論證失敗的精確反例，同時(shí)保留那些經(jīng)受住嚴(yán)謹(jǐn)檢驗(yàn)的好直覺(jué)。

第三階段是“后嚴(yán)謹(jǐn)”階段：你可以在形式化與非形式化之間自如切換。你能夠用非形式化的方式論證，但現(xiàn)在是安全的，因?yàn)殄e(cuò)誤的直覺(jué)已被清除；而且你知道，必要時(shí)可以將其轉(zhuǎn)換回嚴(yán)謹(jǐn)形式。反過(guò)來(lái)，你也能閱讀一個(gè)嚴(yán)謹(jǐn)?shù)恼撟C，并將其翻譯成直覺(jué)性的語(yǔ)言。

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

理想情況下，我們應(yīng)該對(duì)這些假設(shè)進(jìn)行壓力測(cè)試。而 Lean 提供的自動(dòng)檢查器恰好能做到這一點(diǎn)：當(dāng)你形式化某個(gè)證明后，它會(huì)提示你“順便說(shuō)一句，你從未使用過(guò)這些假設(shè)”，有時(shí)這會(huì)帶來(lái)真正的進(jìn)展。人們可能長(zhǎng)期存在某種思維定勢(shì)，認(rèn)為某個(gè)工具只能在特定條件下使用，但證明本身其實(shí)并不依賴那個(gè)條件，只是從未有人注意到。形式化讓我們能夠自動(dòng)發(fā)現(xiàn)每個(gè)工具的自然適用范圍，這非常有價(jià)值。

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

我特別想問(wèn)的是：你在形式化過(guò)程中的“頓悟時(shí)刻”是什么？學(xué)習(xí)一門(mén)小眾的學(xué)術(shù)編程語(yǔ)言顯然需要跨越最初的門(mén)檻，但在什么時(shí)刻你意識(shí)到，將數(shù)學(xué)轉(zhuǎn)化為軟件的過(guò)程本身也能加速理解，甚至推動(dòng)數(shù)學(xué)發(fā)現(xiàn)？對(duì)我而言，這個(gè)時(shí)刻出現(xiàn)在形式化連續(xù)統(tǒng)假設(shè)獨(dú)立性證明的過(guò)程中：我陷入困境，所有源材料都存在問(wèn)題，然后我發(fā)現(xiàn)可以通過(guò)開(kāi)關(guān)某些關(guān)鍵假設(shè)，迅速獲得比任何教科書(shū)都更深刻的理解。我好奇你有怎樣的類(lèi)似經(jīng)歷。

陶哲軒：有兩個(gè)時(shí)刻給我留下了深刻印象。

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

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

第二個(gè)經(jīng)歷來(lái)自另一個(gè)項(xiàng)目“等式理論計(jì)劃”。有人在形式化他人撰寫(xiě)的證明時(shí)在某一步卡住了，說(shuō)：“我不知道怎么處理這一步?！蔽也榭戳四且恍写a。雖然不理解整個(gè)證明，但我能理解那一行及其足夠的上下文，于是告訴他：“你只需要這樣修改這一行，就能使用那個(gè)工具了。”我可以給出非常原子化的診斷——如何修復(fù)一個(gè) 1,000 行代碼中的問(wèn)題，只需檢查其中 3 行。

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

在傳統(tǒng)數(shù)學(xué)中，這種交流只能與那些我完全熟悉的合作者進(jìn)行。我們必須長(zhǎng)期共事，達(dá)到能夠理解彼此思維方式的精細(xì)程度，甚至能夠接續(xù)對(duì)方的話。進(jìn)入那種狀態(tài)是美妙的，但我只與少數(shù)幾位合作者建立了這樣的默契。與新人合作時(shí)，你必須解釋所有定義，還會(huì)產(chǎn)生各種誤解。但有了 Lean，這一切障礙都消失了，因?yàn)槟銚碛袑?duì)問(wèn)題本質(zhì)和解決方案的精確類(lèi)型描述。

它以一種前所未有的方式將數(shù)學(xué)原子化了。

問(wèn)：你是互聯(lián)網(wǎng)數(shù)學(xué)協(xié)作的先驅(qū)之一，包括 Polymath 項(xiàng)目這種眾包數(shù)學(xué)研究的模式。能否談?wù)勀銓?duì)數(shù)學(xué)協(xié)作的理解在過(guò)去 20 年間是如何演變的？以及在這種高度模塊化、有時(shí)甚至匿名的互動(dòng)方式下，數(shù)學(xué)的未來(lái)會(huì)呈現(xiàn)怎樣的面貌？另外，你幾年前在 Notices of the AMS 上發(fā)表的文章中討論了數(shù)學(xué)家角色的演變。我好奇，隨著你組織這些形式化項(xiàng)目，你對(duì)自身角色的理解發(fā)生了怎樣的變化，以及運(yùn)營(yíng) Polymath 項(xiàng)目積累的經(jīng)驗(yàn)如何與此相互作用？

陶哲軒：我一直感到想做的數(shù)學(xué)遠(yuǎn)超個(gè)人所能完成的范圍，因此始終認(rèn)為協(xié)作極具價(jià)值。我從合作者那里學(xué)到了很多，也從互聯(lián)網(wǎng)上的隨機(jī)交流中獲益匪淺。我開(kāi)始寫(xiě)博客源于一次偶然經(jīng)歷：有一次我在個(gè)人網(wǎng)頁(yè)上發(fā)布了一個(gè)數(shù)學(xué)問(wèn)題，并不指望有人回應(yīng)。但那時(shí)已經(jīng)有足夠多的人關(guān)注我的頁(yè)面，三天之內(nèi)我就收到了關(guān)于這個(gè)問(wèn)題來(lái)源的完整文獻(xiàn)索引?，F(xiàn)在這其實(shí)是一個(gè)簡(jiǎn)單的 ChatGPT 查詢就能解決的問(wèn)題，但在當(dāng)時(shí)，這對(duì)我是革命性的。

后來(lái) Tim Gowers 發(fā)起了 Polymath 項(xiàng)目，嘗試眾包數(shù)學(xué)研究，我非常投入。這與我的理念產(chǎn)生了共鳴。參與者越多，就越有可能產(chǎn)生那種任何單個(gè)專(zhuān)家都無(wú)法獨(dú)自發(fā)現(xiàn)的意外聯(lián)系。但這些項(xiàng)目始終存在瓶頸：當(dāng)有一二十人貢獻(xiàn)時(shí)，必須有人檢查所有答案、確保整體連貫并撰寫(xiě)總結(jié)。這個(gè)人要么是我，要么是 Tim Gowers，要么是其他核心成員。這極其消耗精力，你就像星形網(wǎng)絡(luò)的中心節(jié)點(diǎn)。

因此，雖然前景誘人，這種范式終究無(wú)法規(guī)模化。它確實(shí)促成了一些非常廣泛的項(xiàng)目，參與者從數(shù)學(xué)的各個(gè)領(lǐng)域貢獻(xiàn)聯(lián)系，這些領(lǐng)域與項(xiàng)目的關(guān)聯(lián)性是組織者事先完全沒(méi)有預(yù)料到的。但我們?nèi)狈︱?yàn)證的組織基礎(chǔ)設(shè)施。而且當(dāng)時(shí)我們是在博客或 wiki 上運(yùn)營(yíng)，而非像現(xiàn)在這樣使用 GitHub。

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

在傳統(tǒng)數(shù)學(xué)項(xiàng)目中，你可能有一兩位合作者，但即便是協(xié)作，每個(gè)人也必須承擔(dān)所有工作：每個(gè)人都得理解數(shù)學(xué)、都得會(huì)寫(xiě) LaTeX、都得能檢查論證，每個(gè)環(huán)節(jié)每個(gè)人都要參與。而在真正的分工體系中，有專(zhuān)人管理項(xiàng)目、有專(zhuān)人負(fù)責(zé)質(zhì)量保證，就像工業(yè)化生產(chǎn)和專(zhuān)業(yè)化分工那樣。

軟件工程早已想通了這一點(diǎn)。軟件開(kāi)發(fā)過(guò)去也是單槍匹馬的黑客模式，但那種方式無(wú)法支撐大規(guī)模系統(tǒng)。企業(yè)級(jí)軟件需要專(zhuān)精于不同領(lǐng)域的人協(xié)同工作。我預(yù)見(jiàn)數(shù)學(xué)研究也將越來(lái)越多地采用這種規(guī)?；?、專(zhuān)業(yè)化的模式。當(dāng)然，傳統(tǒng)的手工藝式數(shù)學(xué)仍將存在并受到珍視，但我們將擁有這種高度互補(bǔ)的新方式。

問(wèn)：這是否意味著你預(yù)見(jiàn)大多數(shù)職業(yè)數(shù)學(xué)家的角色將演變?yōu)檫@類(lèi)工業(yè)化系統(tǒng)的架構(gòu)師？

陶哲軒：我認(rèn)為“數(shù)學(xué)家”的定義本身將會(huì)拓寬。會(huì)有擅長(zhǎng)運(yùn)營(yíng)大型項(xiàng)目的人，他們是項(xiàng)目經(jīng)理，懂得足夠的數(shù)學(xué)和足夠的 Lean 來(lái)把握高層面的進(jìn)展，但未必能解決具體的技術(shù)細(xì)節(jié)；他們的核心能力在于協(xié)調(diào)大型項(xiàng)目。

會(huì)有一些人特別擅長(zhǎng)形式化，或特別擅長(zhǎng)使用新的 AI 工具，但未必是某個(gè)數(shù)學(xué)分支的領(lǐng)域?qū)＜摇?/p>

人們可以更靈活地加入和離開(kāi)項(xiàng)目。當(dāng)然，你也可以選擇更傳統(tǒng)的方式，讓小團(tuán)隊(duì)里每個(gè)人深度參與所有環(huán)節(jié)。我認(rèn)為這仍然是做數(shù)學(xué)的重要方式之一。

關(guān)鍵在于我們有了選擇。目前，許多熱愛(ài)數(shù)學(xué)的人被排斥在數(shù)學(xué)研究之外，因?yàn)殚T(mén)檻太高了。如果你想?yún)⑴c前沿研究，你需要具備博士級(jí)別的數(shù)學(xué)素養(yǎng)，需要熟練使用 LaTeX，還需要確保寫(xiě)作不出任何差錯(cuò)。這對(duì)許多數(shù)學(xué)愛(ài)好者來(lái)說(shuō)過(guò)于艱巨。而那些確實(shí)嘗試參與的人，常常被當(dāng)作民科打發(fā)，因?yàn)樗麄兊募寄芙M合存在太多缺口。但社會(huì)上確實(shí)存在強(qiáng)烈的需求：數(shù)學(xué)界需要類(lèi)似“公民科學(xué)”的模式。

我現(xiàn)在深度參與一個(gè)叫做“Erd?s 問(wèn)題”的網(wǎng)站，它已經(jīng)發(fā)展成一個(gè)社區(qū)，幾十位不同數(shù)學(xué)教育背景的人在貢獻(xiàn)各種工作。我們找到了模塊化問(wèn)題的方法：也許你無(wú)法解決整個(gè)問(wèn)題，但你可以挖掘相關(guān)文獻(xiàn)、建立與某個(gè)整數(shù)序列的聯(lián)系、評(píng)論他人的證明、進(jìn)行數(shù)值實(shí)驗(yàn)。有一批潛在的人渴望參與研究級(jí)別的數(shù)學(xué)，這些工具有望為他們打開(kāi)大門(mén)。

圖丨Erd?s 問(wèn)題網(wǎng)站（來(lái)源：Erd?s Problem）

問(wèn)：到目前為止，我們討論了你在形式化前沿的經(jīng)驗(yàn)，以及協(xié)調(diào)大規(guī)模數(shù)學(xué)研究的經(jīng)驗(yàn)。我想這是一個(gè)合適的時(shí)機(jī)來(lái)談?wù)勀阏谕苿?dòng)的解析數(shù)論邊界形式化項(xiàng)目。也許我們可以從一個(gè)簡(jiǎn)要說(shuō)明開(kāi)始，讓普通讀者理解為什么這個(gè)問(wèn)題重要，以及它如何體現(xiàn)我們之前討論的這些主題？

陶哲軒：讓我提供一個(gè)思考框架。我傾向于將自動(dòng)化視為人類(lèi)思維的補(bǔ)充工具。使用計(jì)算機(jī)研究數(shù)學(xué)，最顯而易見(jiàn)的方式是拿人類(lèi)想攻克的最難問(wèn)題，比如黎曼假設(shè)，讓計(jì)算機(jī)去嘗試。計(jì)算機(jī)在這類(lèi)人類(lèi)關(guān)注的問(wèn)題上會(huì)取得一定進(jìn)展，但我認(rèn)為，至少在近期，它們?cè)谀切┡c人類(lèi)偏好完全正交的方向上會(huì)更加成功。具體而言，那些涉及大量繁瑣數(shù)值運(yùn)算、需要篩選海量排列組合的工作，人類(lèi)可能不喜歡做，而 AI 完全沒(méi)有這種障礙。

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

我們擁有許多精妙的想法和工具，可以將一類(lèi)關(guān)于數(shù)字、指數(shù)和或黎曼 zeta 函數(shù)的陳述轉(zhuǎn)化為另一類(lèi)我們關(guān)心的陳述。但這些工具都有各自的輸入輸出要求，你需要將它們恰當(dāng)?shù)卮?lián)起來(lái)。你可以在論文中找到這些工具，但每篇論文使用不同的符號(hào)體系，有時(shí)它們的假設(shè)條件與你的需求不完全匹配，于是你不得不拆解原始證明，構(gòu)建自己的版本。

這涉及大量重復(fù)造輪子和參數(shù)調(diào)整的工作，而且容易出錯(cuò)。為了減輕痛苦，我們發(fā)明了一些變通方法。其中之一是聲稱(chēng)“不關(guān)心常數(shù)”：與其寫(xiě)出“這里是常數(shù) 27，那里是常數(shù) 38”，我們統(tǒng)一用 C 表示，只說(shuō)“這是某個(gè)常數(shù)”，不去計(jì)算具體數(shù)值。這減少了計(jì)算量，也在一定程度上防止錯(cuò)誤。如果你在常數(shù)上犯了算術(shù)錯(cuò)誤，但結(jié)論仍然表述為“存在常數(shù) C 使得 ……”，就不會(huì)造成嚴(yán)重后果。

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

因此，只有一小部分被稱(chēng)為“顯式數(shù)論”的領(lǐng)域會(huì)精確計(jì)算所有常數(shù)。這類(lèi)工作更加繁瑣，愿意從事的人更少，相關(guān)論文讀起來(lái)也不愉快，這不是作者的問(wèn)題，而是內(nèi)容本身的性質(zhì)決定的，大量顯式計(jì)算本就不具有文學(xué)性。

但我認(rèn)為這恰恰是自動(dòng)化的理想目標(biāo)。如果我們能建立某種流水線，將這些顯式論文形式化，其中的核心思想和輸入已經(jīng)相當(dāng)清晰，主要挑戰(zhàn)在于匹配眾多略有差異的工具、對(duì)齊所有參數(shù)，我相信這完全在當(dāng)前技術(shù)的能力范圍之內(nèi)。在此基礎(chǔ)上，我們還可以利用 AI 或機(jī)器學(xué)習(xí)來(lái)尋找最優(yōu)的串聯(lián)方式。

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

我們可以擁有一個(gè)動(dòng)態(tài)的、實(shí)時(shí)更新的領(lǐng)域知識(shí)庫(kù)，而非那些寫(xiě)死指數(shù)的靜態(tài)論文。目前，每當(dāng)某個(gè)結(jié)果改進(jìn)，就需要手工重寫(xiě)現(xiàn)有論文來(lái)計(jì)算最新邊界。對(duì)于任何給定的結(jié)果，這種更新大約每 10 年才進(jìn)行一次。但如果有了正確的工具，這可以在幾分鐘內(nèi)完成。

問(wèn)：你是說(shuō)這本質(zhì)上是一個(gè)軟件問(wèn)題。這或許類(lèi)似于早期程序員看待匯編語(yǔ)言的方式——繁瑣，子程序隱藏在代碼中，稱(chēng)不上文學(xué)，但一旦能夠在更高抽象層次上推理 ……

陶哲軒：正是如此。現(xiàn)代軟件原則上是可互操作的：你可以調(diào)用其他模塊，有標(biāo)準(zhǔn)化的接口讓軟件工具相互通信，你可以構(gòu)建大規(guī)模的復(fù)雜生態(tài)系統(tǒng)。當(dāng)然，也因此會(huì)有更多 bug。但有了 Lean，我們有望以一種無(wú) bug 的方式實(shí)現(xiàn)大量研究者之間的互操作。這是目前根本不存在的東西。

問(wèn)：你認(rèn)為數(shù)論或其他領(lǐng)域有多大比例的工作是由這類(lèi)繁瑣活動(dòng)構(gòu)成的？

陶哲軒：這個(gè)比例很難精確量化，而且我認(rèn)為影響是間接的。正因?yàn)榇嬖谶@些繁瑣的計(jì)算，我們實(shí)際上會(huì)下意識(shí)地調(diào)整研究方向來(lái)規(guī)避它們。當(dāng)一條思路開(kāi)始變得計(jì)算量巨大、錯(cuò)綜復(fù)雜時(shí)，我們往往會(huì)繞道而行，轉(zhuǎn)向其他問(wèn)題。所以如果只看論文中呈現(xiàn)的內(nèi)容，繁瑣工作的比例似乎并不高，但那是因?yàn)槲覀円恢痹诶@開(kāi)路上的坑洞。真正的代價(jià)不在于“我們花了多少時(shí)間做苦力”，而在于“我們因?yàn)椴幌胱隹嗔Χe(cuò)過(guò)了多少機(jī)會(huì)”。

我相信當(dāng)這些工具成熟之后，我們將改變做數(shù)學(xué)的方式。遇到大規(guī)模計(jì)算，我們會(huì)直接用技術(shù)工具去攻克它，而不是繞路回避。我們將能夠突破那些現(xiàn)在幾乎是本能般回避的障礙。所以表面的百分比看起來(lái)不高，但如果從錯(cuò)失機(jī)會(huì)的角度衡量，代價(jià)是巨大的。

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

陶哲軒：首先存在信任問(wèn)題。這類(lèi)計(jì)算中，如果某處出現(xiàn)一個(gè)錯(cuò)誤步驟，整個(gè)計(jì)算就作廢了。所以你必須知道誰(shuí)是可靠的作者、誰(shuí)不是。這是隱性信息，我們不會(huì)發(fā)布“不可靠作者名單”。因此，你必須了解這個(gè)社區(qū)，知道該向誰(shuí)請(qǐng)教。如果某個(gè)結(jié)果不完全在文獻(xiàn)中，但你可以問(wèn)某位專(zhuān)家，對(duì)方會(huì)告訴你“對(duì)，只需要這樣修改就行”。這里的瓶頸在于：你必須身處這個(gè)圈子，認(rèn)識(shí)所有關(guān)鍵人物，才能在這個(gè)領(lǐng)域有效地工作。

我認(rèn)為一旦有了形式化帶來(lái)的信任保障，這個(gè)領(lǐng)域就可以更大程度地開(kāi)放。你可以使用素未謀面者的結(jié)果，只要它經(jīng)過(guò) Lean 驗(yàn)證。這將解除大量工作的阻塞。

問(wèn)：你提到了信任這個(gè)概念。一個(gè)研究者在某個(gè)領(lǐng)域持續(xù)工作，隨著時(shí)間推移積累聲譽(yù)和信任。一個(gè)真正激發(fā)我對(duì)形式化和數(shù)學(xué)基礎(chǔ)興趣的故事是沃沃斯基（Vladimir Voevodsky）的經(jīng)歷。他建立了非凡的聲譽(yù)，證明了一系列驚人的結(jié)果，但在 90 年代末發(fā)表的一篇論文中，他大約 10 年后才發(fā)現(xiàn)存在一個(gè)關(guān)鍵錯(cuò)誤。他由此認(rèn)識(shí)到，所有人信任他只是因?yàn)樗休x煌的 track record，但這并不能真正保證正確性。

圖丨沃沃斯基（來(lái)源：WikiPedia）

陶哲軒：正是由于這種不斷累積的信任網(wǎng)絡(luò)存在局限，目前我們能夠推進(jìn)數(shù)學(xué)的深度是有上限的。在分析學(xué)中，這個(gè)問(wèn)題相對(duì)不那么嚴(yán)重，因?yàn)槲覀兊臉?gòu)建方式更加貼近基本原理，更接近第一性原理推導(dǎo)。但它確實(shí)是數(shù)學(xué)整體面臨的一個(gè)制約因素。

問(wèn)：作為后續(xù)問(wèn)題：隨著這個(gè)項(xiàng)目推進(jìn)——從羅瑟（Rosser）和施恩菲爾德（Schoenfeld）等人 1960 年代以來(lái)的經(jīng)典論文開(kāi)始形式化——你認(rèn)為現(xiàn)有文獻(xiàn)中可能存在多少尚未被發(fā)現(xiàn)的錯(cuò)誤？而這些錯(cuò)誤中又有多少只是無(wú)關(guān)緊要的小問(wèn)題，數(shù)學(xué)這一學(xué)科的整體知識(shí)庫(kù)對(duì)它們是具有魯棒性的？

陶哲軒：我很想知道實(shí)際的錯(cuò)誤率是多少。也許結(jié)果會(huì)讓我們欣慰，也許會(huì)令人不安。6 個(gè)月后再問(wèn)我這個(gè)問(wèn)題吧，屆時(shí)我們會(huì)找到答案。

參考資料：

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

運(yùn)營(yíng)/排版：何晨龍