陶哲軒談AI與形式化：數(shù)學(xué)研究的范式革命已經(jīng)開始

近日，Math Inc. 與知名數(shù)學(xué)家陶哲軒進(jìn)行了一場深入對話。作為 2006 年菲爾茲獎得主，他近年來在形式化數(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），陶哲軒正在身體力行地推動一場數(shù)學(xué)研究范式的變革。這次對話中，他坦誠地分享了自己對形式化工具、AI 技術(shù)以及數(shù)學(xué)未來的思考。

（來源：Youtube）

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

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

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

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

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

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

以下是對話全文。

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

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

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

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é)會了使用軟件工程的工具——GitHub、更智能的項(xiàng)目組織方式。

圖丨 Peter Scholze（來源：WikiPedia）

問：那次會議促使你開始學(xué)習(xí) Lean？

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

形式化和 AI 真正實(shí)現(xiàn)的，是讓具有不同技能組合的人能夠無縫協(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é)、都得會寫 LaTeX、都得能檢查論證，每個(gè)環(huán)節(jié)每個(gè)人都要參與。而在真正的分工體系中，有專人管理項(xiàng)目、有專人負(fù)責(zé)質(zhì)量保證，就像工業(yè)化生產(chǎn)和專業(yè)化分工那樣。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

參考資料：

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

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