很多人提到數(shù)學(xué)研究，腦子里浮現(xiàn)的還是那個(gè)畫面：一個(gè)人，一塊白板，來回踱步，等靈感突然降臨。

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

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

▲視頻標(biāo)題：Terry Tao on the future of mathematics

視頻鏈接：https://www.youtube.com/watch?v=4ykbHwZQ8iU

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

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

陶哲軒預(yù)見到，數(shù)學(xué)界將出現(xiàn)類似軟件工程的分工模式。未來的數(shù)學(xué)家可能扮演「架構(gòu)師」或項(xiàng)目經(jīng)理的角色，領(lǐng)導(dǎo)大型協(xié)作項(xiàng)目。這種模塊化的研究方式可能允許「公民數(shù)學(xué)家」（非專業(yè)領(lǐng)域?qū)＜业邆淠承┘寄艿娜耍﹨⑴c到前沿研究中，降低進(jìn)入門檻。如此一來，數(shù)學(xué)研究的進(jìn)展或顯著加速。

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

以下是機(jī)器之心整理的訪談?dòng)涗洝?/p>

從幾十年到 18 個(gè)月

數(shù)學(xué)研究正被加速

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

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

Jared Duker Lichtman：液態(tài)張量實(shí)驗(yàn)。

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

Jared Duker Lichtman： 就是因?yàn)槟谴螘h。

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

Jared Duker Lichtman： 讓人完全上癮。

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

形式化正在改變數(shù)學(xué)思維

把含混經(jīng)驗(yàn)轉(zhuǎn)化為可檢驗(yàn)的結(jié)構(gòu)

Jesse Han： 我第一次接觸 Kevin Buzzard，是 2017 年他在 MSRI（美國數(shù)學(xué)科學(xué)研究所）教自守形式那門課的時(shí)候。幾年后我跟他聊天，他說他當(dāng)時(shí)根本沒在關(guān)注那門課的內(nèi)容，因?yàn)槟莻€(gè)夏天他正在自學(xué) Lean—— 在 Tom Hales 在第一屆大型證明會議上告訴大家 Lean 將是未來之后。

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

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

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

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

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

然后是嚴(yán)謹(jǐn)階段，你被迫完全按照規(guī)矩來，每一步都要做得準(zhǔn)確無誤。但在這個(gè)階段，你往往會失去直覺，因?yàn)槟闳康淖⒁饬Χ荚诖_保每一步都正確。不過這有助于清除你所有錯(cuò)誤的直覺，因?yàn)槟隳芸吹骄_的反例，知道論證在哪里失敗了。而所有好的直覺 —— 那些與嚴(yán)謹(jǐn)推理一致的 —— 都會保留下來。

然后是后嚴(yán)謹(jǐn)階段，你可以在兩種模式之間自由切換。你可以非形式化地論證，但現(xiàn)在是安全的，因?yàn)槟阋呀?jīng)清除了所有錯(cuò)誤的直覺。你知道如果需要的話，可以把它轉(zhuǎn)換回嚴(yán)謹(jǐn)?shù)男问?。反過來，你也可以讀一個(gè)嚴(yán)謹(jǐn)?shù)恼撟C，然后把它轉(zhuǎn)換成直覺性的語言。

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

Jared Duker Lichtman：你會想去對這些假設(shè)進(jìn)行壓力測試。

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

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

兩個(gè)頓悟時(shí)刻

形式化正在改變數(shù)學(xué)領(lǐng)域協(xié)作方式

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

對我來說，是在形式化連續(xù)統(tǒng)假設(shè)的獨(dú)立性時(shí)。有一個(gè)時(shí)刻我完全迷失了，所有的參考資料都是錯(cuò)的，但我發(fā)現(xiàn)可以打開或關(guān)閉某些關(guān)鍵假設(shè)，然后很快就獲得了比任何教科書都深得多的理解。我很好奇你有沒有類似的經(jīng)歷。

陶哲軒：有，我有兩個(gè)印象特別深刻的時(shí)刻。

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

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

后來，有人往 arXiv 上放了一個(gè)很短的預(yù)印本，說如果你回到原始論文，只要做五個(gè)小改動(dòng)，就可以把這個(gè) 12 降到 11。于是大家就開始討論：那我們要不要把 C 等于 11 也形式化一遍？問題在于，C 等于 12 已經(jīng)花了我們?nèi)軙r(shí)間，那再來一遍豈不是又是三周？

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

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

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

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

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

我認(rèn)為這正是 Lean，乃至形式化驗(yàn)證軟件的一大特點(diǎn)：它具有一種高度模塊化的結(jié)構(gòu)，這是很多其他軟件甚至傳統(tǒng)數(shù)學(xué)中并不具備的。你可以圍繞某一行、某一個(gè)非常具體的局部問題展開極其精細(xì)的討論，而完全不需要理解系統(tǒng)的其余部分。

而在傳統(tǒng)數(shù)學(xué)中，只有在與你長期合作、彼此已經(jīng)在思維方式上高度對齊的情況下，才能做到這一點(diǎn)。那種狀態(tài)下，你們幾乎可以在極其細(xì)微的層面上互相理解，甚至補(bǔ)全對方的句子。

通常情況下，當(dāng)你和一個(gè)尚未在思維方式上充分同步的人討論數(shù)學(xué)問題時(shí)，是很難進(jìn)行這種粒度如此之細(xì)的交流的。

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

而在 Lean 中，這些問題在很大程度上都會消失。因?yàn)槟忝鎸Φ氖且粋€(gè)對問題和修復(fù)方式都有著精確定義的類型描述。問題是什么、哪里不匹配、該如何修復(fù)，都被明確地寫進(jìn)了系統(tǒng)里。Lean 以一種此前從未有過的方式，把數(shù)學(xué)原子化了 —— 這是其他做數(shù)學(xué)的方法所不具備的。

數(shù)學(xué)進(jìn)入「工業(yè)化」時(shí)代

數(shù)學(xué)家也可以是架構(gòu)師

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

以及展望未來，在一種高度模塊化的交互模式下，有時(shí)甚至是匿名的協(xié)作中，數(shù)學(xué)研究可能會呈現(xiàn)出怎樣的新形態(tài)？

Jesse Han：我想再補(bǔ)充一點(diǎn)。你在幾年前發(fā)表于《Notices of the American Mathematical Society》的一篇文章里，提到過一個(gè)非常有意思的觀點(diǎn)：你如何看待數(shù)學(xué)家角色的演變。

我也很想聽你進(jìn)一步展開這一點(diǎn)，因?yàn)檫@和我們剛才討論的內(nèi)容高度相關(guān)，比如，當(dāng)你開始主導(dǎo)、協(xié)調(diào)這些形式化項(xiàng)目時(shí)，你是否也感受到自己角色的變化？以及你在組織 Polymath 項(xiàng)目過程中積累的經(jīng)驗(yàn)，又是如何與這種變化發(fā)生交匯、相互影響的？

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

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

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

但與此同時(shí)，這種協(xié)作方式始終存在一個(gè)明顯的瓶頸。

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

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

陶哲軒：對，這種模式雖然很有潛力，但并沒有真正實(shí)現(xiàn)規(guī)?；２贿^，它確實(shí)促成了一些非常宏大的研究項(xiàng)目：來自數(shù)學(xué)中完全不同方向的人，會因?yàn)榕既坏撵`感，貢獻(xiàn)出大量有價(jià)值的線索。很多時(shí)候，項(xiàng)目的組織者事先根本不知道這些人彼此之間存在任何關(guān)聯(lián)，但他們提供的想法卻是相關(guān)且有用的。

問題在于，當(dāng)時(shí)我們并沒有完善的組織與驗(yàn)證基礎(chǔ)設(shè)施。而且那時(shí)我們主要是通過博客和 Wiki 來運(yùn)作項(xiàng)目，而不是像今天這樣使用 GitHub 這類更成熟的協(xié)作平臺。

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

這也使得數(shù)學(xué)研究第一次真正具備了分工協(xié)作的可能性。

在傳統(tǒng)數(shù)學(xué)研究中，無論是單人還是合作，參與者幾乎都需要什么都懂：既要理解全部數(shù)學(xué)內(nèi)容，又要會寫 LaTeX、檢查推導(dǎo)、整理論文，每個(gè)人都要覆蓋所有環(huán)節(jié)。而在真正意義上的分工體系中，就像工業(yè)化生產(chǎn)一樣，會有人負(fù)責(zé)項(xiàng)目管理，有人負(fù)責(zé)質(zhì)量驗(yàn)證，有人專注于具體技術(shù)細(xì)節(jié)。

軟件工程其實(shí)早就完成了這種轉(zhuǎn)變。早期的軟件開發(fā)也是一個(gè)人包辦一切，但這種方式無法擴(kuò)展；一旦進(jìn)入企業(yè)級開發(fā)，就必須依賴高度專業(yè)化的角色分工。

因此，我確實(shí)預(yù)見到一種趨勢：在規(guī)模化、工業(yè)化的條件下生產(chǎn)數(shù)學(xué)成果，并且伴隨著清晰的專業(yè)分工。當(dāng)然，傳統(tǒng)的、手工式的數(shù)學(xué)研究依然會存在，也依然會被高度珍視；只是未來會出現(xiàn)一種與之互補(bǔ)的、全新的數(shù)學(xué)生產(chǎn)方式。

Jesse Han：那么，這是否意味著你預(yù)見到，大多數(shù)職業(yè)數(shù)學(xué)家的角色將會演變?yōu)檫@些工業(yè)化數(shù)學(xué)體系的架構(gòu)師？

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

同時(shí)，也會有一些人，他們可能并不是某個(gè)數(shù)學(xué)領(lǐng)域的專家，但非常擅長形式化工作，或者非常善于使用新的 AI 工具。這些能力本身同樣有價(jià)值。

在這樣的體系中，人們可以更自由地加入或離開項(xiàng)目，協(xié)作將變得更加流動(dòng)。當(dāng)然，也仍然會存在更傳統(tǒng)的研究方式：由一個(gè)規(guī)模較小的團(tuán)隊(duì)組成，所有人都深度參與項(xiàng)目的每一個(gè)環(huán)節(jié)。這種方式依然非常重要，也不會消失。關(guān)鍵在于，我們終于擁有了多種選擇。

在當(dāng)前體系下，許多真正熱愛數(shù)學(xué)的人被擋在數(shù)學(xué)研究之外，只是因?yàn)殚T檻太高了。如果你想?yún)⑴c前沿研究，就必須掌握博士階段水平的數(shù)學(xué)；你還得會用 LaTeX；得知道如何寫作、如何避免任何細(xì)節(jié)錯(cuò)誤…… 這些要求疊加在一起，對很多人來說極具威懾性，進(jìn)入門檻過高。

即便成功進(jìn)入這一體系的人，也常常因?yàn)樽陨砑寄芙Y(jié)構(gòu)不完整而被忽視或邊緣化。但未來并不必然如此，隨著工具、形式化和協(xié)作方式的變化，這種狀況有可能被根本性地改變。

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

陶哲軒：是的，我們其實(shí)已經(jīng)在看到這種趨勢了。比如我自己就深度參與過一個(gè)數(shù)學(xué)問題網(wǎng)站。它逐漸發(fā)展成了一個(gè)社區(qū)，聚集了幾十位數(shù)學(xué)背景和受教育程度各不相同的參與者，大家各自貢獻(xiàn)一些小而具體的內(nèi)容。

我們學(xué)會了把一個(gè)問題模塊化拆解：也許你沒法完整地解決這個(gè)問題，但你可以幫忙查找相關(guān)參考文獻(xiàn)；或者把問題和某個(gè)整數(shù)序列聯(lián)系起來；或者評論、改進(jìn)他人的證明；又或者做一些數(shù)值實(shí)驗(yàn)和計(jì)算。

正是通過這種方式，很多人都能在自己能力范圍內(nèi)參與進(jìn)來。

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

AI 應(yīng)該先幫數(shù)學(xué)家「干臟活」

Jesse Han：到目前為止，我們已經(jīng)談了很多內(nèi)容：一方面是你在形式化數(shù)學(xué)前沿工作的經(jīng)驗(yàn)，另一方面是你在協(xié)調(diào)大規(guī)模協(xié)作項(xiàng)目、加速數(shù)學(xué)研究方面的實(shí)踐。而我覺得，正好在這兩者的交匯點(diǎn)上，是一個(gè)非常合適的時(shí)機(jī)，來談?wù)勀隳壳疤貏e投入、也非常興奮推動(dòng)的一個(gè)項(xiàng)目，解析數(shù)論中數(shù)學(xué)界限（Bounds）的形式化證明。

或許我們可以從一個(gè)簡要的介紹開始：面向非專業(yè)讀者，能否先解釋一下 —— 為什么這個(gè)問題本身如此重要？以及它在某種程度上，如何成為我們剛才討論過的那些問題（協(xié)作、形式化、規(guī)?；芯浚┑囊粋€(gè)縮影或體現(xiàn)？

陶哲軒：我想先從一個(gè)更宏觀的角度來講。我一直認(rèn)為，自動(dòng)化本質(zhì)上是對人類思維的補(bǔ)充工具。

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

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

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

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

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

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

在這個(gè)過程中，就會產(chǎn)生大量的重復(fù)勞動(dòng)：反復(fù)調(diào)整參數(shù)、對齊條件、重建推導(dǎo)鏈條，而且非常容易出錯(cuò)。

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

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

因此，真正去顯式計(jì)算所有常數(shù)的解析數(shù)論研究，只占整個(gè)領(lǐng)域中非常小的一部分。這類工作極其繁瑣、計(jì)算量巨大，做的人很少，論文也往往不太好理解。這并不是作者水平的問題，而是因?yàn)檠芯績?nèi)容本身就充斥著大量細(xì)碎、明確的計(jì)算過程，幾乎沒有那種直觀的結(jié)構(gòu)美感可言。

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

在此基礎(chǔ)上，我們甚至可以引入 AI 或機(jī)器學(xué)習(xí)，去探索這些工具鏈的最優(yōu)組合方式。這將為整個(gè)領(lǐng)域打開許多全新的觀察視角。

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

這樣一來，我們就可以擁有一個(gè)持續(xù)演化、動(dòng)態(tài)更新的領(lǐng)域最前沿狀態(tài)，而不再是那些寫死了指數(shù)和常數(shù)的論文?，F(xiàn)在的做法是：每當(dāng)某個(gè)關(guān)鍵結(jié)果被改進(jìn)，研究者往往需要重寫整篇論文，重新推導(dǎo)所有相關(guān)界限，才能弄清楚最新的最好結(jié)果是什么。而這類更新，通常十年才發(fā)生一次；但如果工具鏈足夠成熟，這些工作完全可以在幾分鐘內(nèi)完成。

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

陶哲軒：可以這么理解。而且在現(xiàn)代軟件工程中，原則上一切都是可以互操作的。你可以調(diào)用別人的子程序，不同工具之間有標(biāo)準(zhǔn)化的接口和格式，它們能夠彼此通信，從而構(gòu)建起極其復(fù)雜、龐大的軟件生態(tài)系統(tǒng)。

當(dāng)然，這樣的系統(tǒng)也會帶來一個(gè)問題：正是因?yàn)橄到y(tǒng)復(fù)雜、組件眾多，軟件中不可避免會出現(xiàn)各種錯(cuò)誤。

但在數(shù)學(xué)形式化這件事上，像 Lean 這樣的工具，至少在理論上，讓我們有機(jī)會構(gòu)建一種盡可能無 bug 的協(xié)作體系。通過形式化驗(yàn)證，你可以希望、甚至確信這些由大量研究者共同構(gòu)建的成果是相互兼容、邏輯一致的。而這正是我們目前在數(shù)學(xué)研究中所缺失的東西：一種真正可靠、可互操作、可規(guī)?；瘮U(kuò)展的基礎(chǔ)設(shè)施。

當(dāng)新工具出現(xiàn)

數(shù)學(xué)的研究路徑會整體改寫嗎？

Jared Duker Lichtman：那么你是否愿意做一個(gè)大致的判斷或推測：在數(shù)論，乃至其他數(shù)學(xué)領(lǐng)域中，有多大比例的工作其實(shí)是由這些相對枯燥、機(jī)械性的勞動(dòng)構(gòu)成的？如果這種工作負(fù)擔(dān)的比例發(fā)生改變，是否可能由此催生一種截然不同的研究工作流程？

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

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

如果是這樣的話，那么我們是否也可以把如今的形式化工具（如 Lean）以及自動(dòng)形式化技術(shù)，視為歷史上這一類技術(shù)演進(jìn)的又一個(gè)實(shí)例，一次新的數(shù)學(xué)技術(shù)革命？

陶哲軒：我認(rèn)為數(shù)論其實(shí)是最早采用實(shí)驗(yàn)性方法的數(shù)學(xué)分支之一。例如，數(shù)論中的一個(gè)核心問題，關(guān)于素?cái)?shù)分布的規(guī)律，最早就是由高斯提出的猜想。

高斯當(dāng)年通過一種極其艱苦的方式來獲得直覺：他手工計(jì)算了前幾十萬、甚至上百萬個(gè)素?cái)?shù)，并從這些數(shù)據(jù)中觀察到了某些模式，由此提出了后來影響深遠(yuǎn)的素?cái)?shù)分布猜想。

從今天的角度看，這幾乎就是一種早期的計(jì)算實(shí)驗(yàn)數(shù)學(xué)：通過大量具體數(shù)據(jù)的積累，來引導(dǎo)理論判斷和猜想的形成。這在當(dāng)時(shí)是非常開創(chuàng)性的做法，也深刻影響了數(shù)論此后的發(fā)展方向。

Jared Duker Lichtman：而且當(dāng)時(shí)所依賴的，其實(shí)只是規(guī)模很小的數(shù)據(jù)。

陶哲軒：是的。高斯展現(xiàn)出了一種非凡的能力：他能夠從規(guī)模非常小的數(shù)據(jù)集中，概括出極其深刻、普遍的規(guī)律，這正是高斯天才的體現(xiàn)，也正因?yàn)槿绱?，后來很多工具都會以他的名字命名?/p>

而隨著計(jì)算技術(shù)的發(fā)展，我們才真正能夠系統(tǒng)性地展開這種探索。后來也陸續(xù)出現(xiàn)了不少類似的例子：一些重要的猜想最初正是通過數(shù)值實(shí)驗(yàn)和計(jì)算探索被發(fā)現(xiàn)的；而在更近的時(shí)代，還有一些結(jié)果是借助大規(guī)模枚舉，甚至結(jié)合機(jī)器學(xué)習(xí)方法，才逐漸顯現(xiàn)出其結(jié)構(gòu)和規(guī)律的。

這些進(jìn)展都說明了一點(diǎn)：新的技術(shù)手段不斷擴(kuò)展著數(shù)學(xué)家可探索的空間，也在持續(xù)改變?nèi)藗兝斫夂脱芯繑?shù)論的方式。

Jared Duker Lichtman：我想，甚至連圖靈當(dāng)年也在做類似的事情，親自去計(jì)算函數(shù)的零點(diǎn)。

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

因此，歷史上早就存在這樣的先例：計(jì)算機(jī)的引入，催生了一種新的數(shù)學(xué)研究方式，不再只是依賴純粹的抽象思考，而是結(jié)合數(shù)據(jù)和實(shí)驗(yàn)來推動(dòng)理論的發(fā)展。

當(dāng)然，我們現(xiàn)在討論的這種形式化工作，并不完全等同于數(shù)據(jù)驅(qū)動(dòng)的數(shù)學(xué)，但它無疑是一種計(jì)算機(jī)輔助的研究模式。

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

陶哲軒：這個(gè)問題其實(shí)很難給出一個(gè)精確的百分比，但我覺得關(guān)鍵并不在于直接統(tǒng)計(jì)時(shí)間比例，而在于一種間接影響。

正是因?yàn)檫@些繁瑣勞動(dòng)的存在，我們往往會有意識地改變做數(shù)學(xué)的方式，盡量減少自己要面對的苦工。比如，當(dāng)我們意識到某一步組合推導(dǎo)開始變得非常凌亂、計(jì)算量巨大時(shí)，往往會選擇刻意繞開，改用另一條思路繼續(xù)推進(jìn)。

因此，如果你只看最終論文里呈現(xiàn)出來的內(nèi)容，會覺得我們似乎做的都是高判斷力的工作，真正的苦工并不多。但那是因?yàn)槲覀冊谘芯窟^程中，已經(jīng)下意識地避開了道路上的一個(gè)個(gè)坑，用一個(gè)比喻來說，我們是在不斷繞開崎嶇路段，而不是去填平它們。

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

這樣一來，我們就可以穿越那些現(xiàn)在幾乎是下意識回避的障礙。所以，從表面上看，當(dāng)前數(shù)學(xué)研究中苦工的比例似乎并不高；但如果把那些被我們主動(dòng)規(guī)避掉的工作也算進(jìn)去，那這個(gè)比例其實(shí)遠(yuǎn)比看上去要大得多。

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

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

以及，如果你所設(shè)想的這一愿景真的實(shí)現(xiàn)了形式化、自動(dòng)化工具能夠承擔(dān)起這些傳遞與整合工作，你認(rèn)為這一領(lǐng)域的數(shù)學(xué)研究整體上有可能被加速多少倍？

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

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

這就形成了一個(gè)明顯的瓶頸：你必須身處這個(gè)關(guān)系網(wǎng)絡(luò)之中，認(rèn)識足夠多對的人，才能高效地在這個(gè)領(lǐng)域工作。

而一旦我們能夠通過形式化工具（比如 Lean）提供這種可驗(yàn)證的信任保證，情況就會發(fā)生根本改變。那時(shí)，你可以放心使用來自陌生研究者的結(jié)果，即便你從未見過他們，因?yàn)樗凶C明都已經(jīng)由系統(tǒng)嚴(yán)格驗(yàn)證過。

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

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

而真正讓我開始對形式化和數(shù)學(xué)基礎(chǔ)問題產(chǎn)生強(qiáng)烈興趣的一個(gè)重要故事，正是關(guān)于一位數(shù)學(xué)家的經(jīng)歷。他曾經(jīng)建立起極高的學(xué)術(shù)聲譽(yù)，證明過許多非常了不起的結(jié)果，因此在學(xué)界擁有極強(qiáng)的可信度。

但在 20 世紀(jì) 90 年代末，他寫過一篇論文，后來大約在十年之后，他才意識到其中存在一個(gè)關(guān)鍵性的錯(cuò)誤?；剡^頭來看，他自己也反思到：當(dāng)時(shí)很多人之所以接受那篇結(jié)論，很大程度上是因?yàn)榇蠹以谙嘈潘@個(gè)人，而不是因?yàn)樽C明本身被徹底、逐行地驗(yàn)證過。

而這正揭示了一個(gè)核心問題：個(gè)人聲譽(yù)和過往記錄，并不等同于真理的保證。這類經(jīng)歷也正是形式化證明與基礎(chǔ)工具如此重要的原因之一，它們提供的不是基于人的信任，而是基于可驗(yàn)證結(jié)構(gòu)的信任。

陶哲軒：當(dāng)然，這種做法在深度上是有極限的。我們能夠推動(dòng)數(shù)學(xué)前進(jìn)的程度，終究會受到限制。當(dāng)前在分析學(xué)中，這個(gè)問題相對沒那么嚴(yán)重，是因?yàn)檫@里逐漸形成了一張不斷加密的信任之網(wǎng)，而且我們的工作方式往往更接近從第一性原理出發(fā)，比其他一些領(lǐng)域更少依賴遠(yuǎn)距離的結(jié)果。

但即便如此，這種基于信任的結(jié)構(gòu)依然是數(shù)學(xué)發(fā)展的一個(gè)限制因素。從長遠(yuǎn)來看，這是一個(gè)無法回避的問題，也是形式化和基礎(chǔ)工具之所以重要的又一個(gè)原因。

Jared Duker Lichtman：我想再追問一個(gè)相關(guān)的問題。隨著我們開始系統(tǒng)性地回溯并形式化一些經(jīng)典論文，以及從 20 世紀(jì) 60 年代以來的大量文獻(xiàn)，你會如何看待這樣一個(gè)問題：

第一，在現(xiàn)有的數(shù)學(xué)文獻(xiàn)中，可能還存在多少尚未被發(fā)現(xiàn)的錯(cuò)誤？

第二，這些錯(cuò)誤中，有多少只是可以通過小修小補(bǔ)解決的技術(shù)性問題？換句話說，整個(gè)數(shù)學(xué)體系作為一個(gè)整體，對這類錯(cuò)誤究竟有多強(qiáng)的魯棒性？

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

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

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

文章來源：機(jī)器之心。