一位菲爾茲獎得主，成為數學領域人工智能的布道者

借助自動化證明檢查器，一個難題可以被分解成小塊，逐塊解決，然后重新組合，并確信每一部分都是正確的。對一些人而言，這預示著數學研究的一個新領域。

撰文｜Kevin Hartnett

編譯｜數學家編譯小組

諸如 Lean 之類的自動化證明檢查器可以提供鐵一般的保證，確保數學證明是有效的。丨圖源：Samuel Velasco/Quanta Magazine

陶哲軒從不畏懼非傳統的想法。2014 年 11 月，他與另外四位杰出數學家一同出席了一個專家小組討論會，他們都是首屆突破獎數學獎的獲得者，該獎項附帶 300 萬美元的獎金。這些獲獎者的談話內容廣泛，從數學是被發明的還是被發現的——大多數數學家都同意，至少從感覺上像是一種發現行為——到評估我們生活在數字模擬中的可能性。“是啊，我覺得我們其實不是真實的，”Maxim Kontsevich 說，他在 20 世紀 90 年代于數學和物理學的交叉領域做出了自己最重要的研究。

然而，在 40 分鐘的討論過程中，最令人難以置信的言論來自陶哲軒。他預測，在未來，數學家們可能不再獨自或與兩三個人的小團隊合作，而是可能同時與數百名其他人一起參與項目。他還以他謙遜、低調的方式說，當這些合作結束時，其結果可能不是由人類審稿人，而是由計算機來檢驗。“有朝一日，我們可能不再用 LaTeX 寫論文，而是用某種能由智能軟件轉換為形式語言的編程語言來寫，每當你寫錯時，你會得到一個編譯錯誤——計算機不明白你是如何推導出這一步的，”他說。

The Proof in the Code 探索了人類與計算機數學協作的時代。丨圖源：Samuel Velasco/Quanta Magazine

這番言論讓活動主持人和其他獲獎數學家都覺得荒謬至極，以至于相比之下，活在模擬世界的假說反而顯得合理了。比起數百位數學家一起工作這個想法本身，更令人驚訝的是這種合作會吸引陶哲軒——因為如果說世界上有誰似乎特別適合單干的話，那就是他了。

陶哲軒 1975 年出生于澳大利亞的阿德萊德，他的父母在三年前從香港移民到這個國家。很早時候，他們的長子就顯露出了與眾不同的跡象。陶哲軒兩歲時，家人帶他去朋友家做客，結果發現他和幾個六歲的孩子聚在一起，正在用木塊演示如何數數。當被問及如何學會數東西時，他回答說是在《芝麻街》（Sesame Street）上看到的。五年后，陶哲軒七歲時，他開始學習微積分。

1985 年春天，陶哲軒的父母帶他來到美國，為期三周，期間他見到了當時在 Johns Hopkins 大學的“數學早慧少年研究”項目負責人 Julian Stanley。Stanley 稱陶哲軒擁有他見過的“最出色的數學能力”。同年，陶哲軒還結識了 著名數學家 Paul Erd?s，他當時正在阿德萊德訪問。有一張著名的照片，當時 Erd?s 正在閱讀膝上的一份文件，而年僅10歲、有著濃密黑發的陶哲軒則專注地看著，手指若有所思地舉到下巴邊。Erd?s 當時72歲，就像陶哲軒的爺爺。

陶哲軒的少年傳奇在1986年他參加國際數學奧林匹克競賽（IMO）時進一步增長。他在第一次參加就獲得了銅牌，成為有史以來達到這一成績的最年輕參賽者，時年 10 歲。在接下來的兩年里，他先后成為最年輕的銀牌得主，并最終成為最年輕的 IMO 金牌得主。他的正規教育也以同樣以加速的節奏進行。他 15 歲時從阿德萊德當地的 Flinders University 畢業，并于1992年秋天與父親一起登上飛往新澤西州的飛機，開始了他在 Princeton University 的數學博士生涯。Erd?s 曾支持陶哲軒提前進入該項目，并在推薦信中寫道：“我相信他將會成長為一位一流的數學家，或許是一位真正偉大的數學家。”

當時72歲的 Paul Erd?s 與10歲的陶哲軒在一起。丨圖源：Billy Grace Tao 供圖

Erd?s 說得沒錯。到陶哲軒24歲時，他已經做出了足夠多的新發現，可以自主選擇終身教職崗位；他最終決定在 University of California, Los Angeles 安頓下來。大約在那時，他遇到了一位名叫 Ben Green 的年輕英國數論學家。兩人開始合作證明：在大量質數集合中，必然會以某種方式出現某些模式，即算術級數（集合中的數字按固定間隔遞增，例如 7，10，13，16），盡管質數看似隨機地分布在數軸上。他們的證明成為陶哲軒早期職業生涯的標志性成果，為他贏得了 2006 年的菲爾茲獎，并將他推向了數學界的頂端。

陶哲軒本可以不與任何人合作就建立起成功的職業生涯，但他不喜歡那種工作方式。他將與其他研究者合作視為發現新思想的主要途徑——把你所知道的和我所知道的結合起來，看看會發生什么。

這種方法使得陶哲軒的數學研究涵蓋了異常廣泛的主題，從解析數論（包括關于質數的 Green-Tao 定理），到分析學（他研究了描述流體行為的 Navier-Stokes 方程的性質），再到根據數字數據構建 MRI 圖像的算法（這項 MRI 合作是在陶哲軒與當時在 California Institute of Technology 的統計學家 Emmanuel Candès 各自送孩子去幼兒園的談話中發展起來的）。這種對合作探索新知的渴望也促使陶哲軒在公共平臺上進行了大量工作。2007年，他開通了一個博客，開始定期發布關于自己研究的最新動態。到那時，陶哲軒不僅是他所在的領域，更是世界上最著名的數學家之一。他的博文受到了很多關注，有時會在評論區引發長時間的討論，陶哲軒也會熱情地參與其中。他這樣做是因為他覺得這很有趣，同時也希望這些對話能產生新的想法。

大約在同一時間，另一位早期的數學博主也有類似的想法。與陶哲軒一樣，Timothy Gowers 也是一位杰出的研究型數學家，喜歡公開交流。不過， Gowers 并不將希望寄托于博客評論區偶然出現的機會，而是希望以一種有組織的方式引導公眾的活力。2009 年 1 月，他發表了一篇博文，宣布他希望能促成一種新型的“大規模協作數學”。他會在一個開放的在線論壇上提出一個問題，“任何對此問題有見解的人都可以參與進來”。他將其命名為 Polymath Project。

陶哲軒立即加入了進來。和 Gowers 一樣，他知道有些數學問題比其他問題更適合通過大規模協作來解決。關鍵在于，正如陶哲軒在 Gowers 初始博文的評論中所寫，要找到那些能夠“產生大量更簡單的子問題……而這些子問題很大程度上可以并行處理”的問題。通過將大問題分解成獨立的部分，不同的團隊或個人就可以獨立工作，然后將各自的成果作為整體的一部分進行整合。同時，陶哲軒也明白，Polymath 模式可能面臨的最大挑戰在于組織：協調大家的貢獻，并檢查確保所有貢獻都是正確的。

對于第一個 Polymath 項目，Gowers 提出了改進一個名為 Hales-Jewett 定理的結果，該定理涉及用兩種不同顏色中的一種對網格中的單元格進行著色，會出現什么模式。經過幾個月的工作，通過數十位數學家的數千條評論進行協調，該小組證明了一個更精確的陳述——關于這些著色模式是如何出現的。那年秋天，他們以“D. H. J. Polymath”這個化名發表了這項成果，成為了一篇史無前例的數學論文。Gowers 的實驗成功了。它讓許多數學家（無論是專業人士還是業余愛好者）能夠共同工作，并最終產生了一個證明。

在接下來的十年里，又陸續開展了 15 個 Polymath 項目，其中一些由陶哲軒領導，該計劃也引起了主流媒體關注。2011 年 10 月 29 日，The Wall Street Journal 刊登了一篇題為“The New Einsteins Will Be Scientists Who Share”的文章，報道稱 Polymath Project“開創了解決問題的新方法”。

一張解釋證明輔助工具結構的圖示（不知為何，章魚表情符號成了 Lean 社區里表達開心的御用符號)。Samuel Velasco丨圖源：Samuel Velasco/Quanta Magazine

不過從在其他方面看，Polymath Project 其實是一個超前于時代的理念。陶哲軒置身于數學活動熱潮的中心，這令他興奮不已，但他也認識到博客的評論區作為一個協作平臺是有限的。大規模開放協作增加了某種偶然發現的可能性，但同時也提高了參與者犯錯的風險。防范錯誤的唯一方法是讓協調員（版主）仔細檢查所有的工作。但這種審核協調機制破壞了 Polymath 的愿景。

陶哲軒真正追求的是一種高效的、新型的科學發現形式。過了一段時間，他開始意識到 Polymath 模式并非如此。他認為，要實現這一目標，需要某種計算機驗證——一種自動檢查成果的方法，而不是手工檢查。但鑒于 2010 年代的技術水平，他這個愿望就像有載客飛船去火星一樣遙不可及。

陶哲軒了解計算機驗證數學已有多年。他知道一些成功的案例，但也知道形式化數學在當時仍然不切實際，所需付出的努力遠超其帶來的價值，在大多數情況下得不償失。盡管如此，陶哲軒仍對其潛力很感興趣。在世界頂尖數學家中，他幾乎是唯一一個看到了數學新方法潛力的人。

2022 年 7 月，部分出于好奇，他組織了一個研討會，探討計算機輔助數學研究的各種不同方式。他發起了一個聯合組織者團隊，其中包括 Kevin Buzzard，他當時是世界上最引人注目的形式化數學布道者。

在會議召開前夕，陶哲軒認為 Lean（一種允許數學證明像計算機代碼一樣編寫和檢查的軟件）是一個復雜的程序，需要數月時間學習。Buzzard 說服他嘗試一下。在這樣的鼓勵下，陶哲軒感到了一種強烈的責任感，要以身作則——如果要繼續推廣機器輔助證明，必須先從自己開始嘗試。

2023 年 10 月 9 日，陶哲軒在社交媒體上發帖：“我最終決定要熟悉一下 #Lean4 交互式證明系統（必要時會借助人工智能輔助來幫助我使用它）。”

在 MathOverflow（一個頗受數學家歡迎的在線論壇）上，陶哲軒發現了一個關于 Maclaurin 不等式的問題。他決定回答這個問題，作為形式化的一次實驗。首先，他像寫普通數學論文一樣寫出了證明，很短，只有10頁。然后他把注意力轉向了他真正的目標：看看能否用 Lean 將這個簡單的證明形式化。

起初，陶哲軒認為他可能在一周內完成，但他很快就直面用手寫數學公式和用 Lean 輸入數學之間的差異。陶哲軒觀察到，證明中困難的部分在 Lean 中很容易形式化，而簡單的部分卻需要驚人的工作量。

在普通論文中，陶哲軒無需特意說明：如果你有三個數字，每個都大于1 ，那么它們的和必然至少是 3。但 Lean 不能直接接受這樣的斷言，陶哲軒不得不花時間在 Mathlib（一個已經形式化數學的數字庫，Lean 用戶在編寫證明時會用到它）中尋找一個引理來證明這個不言自明的關系。類似地，在非形式化數學中，并不總是需要指定你使用的是哪個數系。例如，數字3同時是一個整數、一個自然數和一個實數。在他最初的論文中，陶哲軒可以直接寫“3”，而不必指明他腦中所想的是哪種3。然而，在 Lean 中，他必須明確說明。陶哲軒發現他的證明一直無法編譯成功，因為他在形式化時的不同步驟里忽略了指定正確的類型。直到將近一個月后的 11 月 6 日，陶哲軒才在他的博客評論中寫道：“只是提一下，我已經成功地將這篇論文的結果在 Lean4 中形式化了。”結果微不足道，他用來形式化它的 Lean 代碼也很糟糕。盡管如此，陶哲軒現在正式成為了 Lean 社區有貢獻的成員。

在學習 Lean 的同時，陶哲軒還在繼續從事許多其他研究項目。其中包括一個與他長期合作者 Ben Green、Timothy Gowers 以及 Freddie Manners（Green 以前的學生，現為 University of California, San Diego 教授）合作的項目。這是一個精英合作團隊——Gowers 和陶哲軒一樣，曾獲得菲爾茲獎，而 Green 是該領域最有成就的數論學家之一。

這個團隊瞄準了一個特定的問題，該問題圍繞著一個稱為“和集”（sumset）的數學對象展開。如果你有一組數，可以用它來形成另一個相關的集合：它的和集。和集是通過取第一個集合中每一對不同的數之和構成的。所有這些和共同構成了原始集合的和集。

如果原始集合的數都是隨機的，那么它的和集會相對較大。一個有 10個隨機數的集合，其和集大約有50個數；一個有1000個數的集合，其和集大約有500,000個數。但是，如果原始集合不是包含隨機數，而是遵循某種模式，那么它的和集會小得多，因為許多和會多次出現，并且每個和在和集中只計入一次。數字1到10的集合就是一個例子——它的和集只包含17個數（而不是像10個隨機數集合那樣預期的50個），因為許多和會重復1+6，2+5，3+4和都等于7，并且在和集中只計入7一次。

除了具有小的和集之外，數字 1到10 也是一個算術級數的例子，因為它們按恒定間隔遞增。20 世紀 60 年代，計算機科學家 Katalin Marton 提出一個猜想，并認為這并非巧合。她預測，產生小和集的集合也必然包含長的算術級數。Gowers、Green 和陶哲軒在21世紀初對一個該問題的精細化版本——Freiman-Ruzsa 多項式猜想取得了進展，但最終還是卡住了。2023年，陶哲軒、Green 和 Manners 再次拾起這個問題，打算引入 Manner 發展的概率論技術。

他們意識到，將這些技術與 Gowers 早期的想法結合起來，或許能解決整個問題。他們邀請 Gowers 加入合作，這個四人組在 2023 年夏天取得了穩步進展。到了深秋，他們成功了。11 月 9 日——就在陶哲軒將他第一個正式的 Lean 證明上傳到 GitHub 的三天后——他們將證明上傳到了 arxiv.org。

由于心中惦記著 Lean，陶哲軒向他的三位合著者建議，可以嘗試將他們的論文形式化。這項工作似乎是一個很好的形式化候選，既因為它是一個重要的成果，也因為它依賴于相對簡單的技術。他們不必花費數月向 Mathlib 添加先決材料——大多數必要的定義已經存在了。

然而，Green、Gowers 和 Manners 并不特別感興趣花時間去學習 Lean。于是陶哲軒獨自開始了——盡管他知道他可能不會獨自一人很久。任何由他領導的項目都可能引起關注。

11 月 13 日，陶哲軒在一個專注于 Lean 的聊天群中開啟了一個新頻道。“大家好。我正在考慮啟動一個項目，在 Lean4 中將 Timothy Gowers、Ben Green、Freddie Manners 和我本人最近對多項式 Freiman-Ruzsa（PFR）猜想的證明形式化，”他寫道。他會利用這個頻道來協調該項目的工作，并且“歡迎任何愿意幫忙的人以他們力所能及的方式為該項目做出貢獻”。這是 Polymath Project 的重啟，只不過這一次他們是在形式化一個已有的成果，而不是試圖證明一個新的成果——而且所有的工作都將由 Lean 驗證，這意味著陶哲軒不必親自檢查。

一天之內，Stockholm University 的博士生 Ya?l Dillies 就為該項目建立了一個粗略的框架，將證明分成了 13 個部分。在每個部分中，陶哲軒確定了需要形式化的引理和定義的序列。在一篇典型的數學論文中，引理（有助于構建更大定理證明的更簡單的成果）可能有大約20行，但對于 PFR 的形式化，陶哲軒將證明分解成了只有 5 行的引理。他的目標是使證明盡可能模塊化，讓更多人能夠做出小的貢獻。

在第一周，論壇上的大部分活動都是關于形式化概率論中的基本概念，這些概念是證明所需的，但 Mathlib 中還沒有。特別是，他們必須形式化香農熵——對數據源（如一組數字）中不確定性或無序程度的度量。除了進行數學形式化的工作之外，陶哲軒和其他人還在第一周花費時間弄清楚如何協同工作。起初，大家的交流比較自由，陶哲軒發帖說明他認為需要做什么，其他人則提出關于如何做的想法，很大程度上就像 Polymath 項目在博客評論中展開的那樣。

11 月 22 日，陶哲軒列出了22個待解決的引理，并寫道：“如果你想申領這些引理中的一個或多個，請在此帖中回復。”回復紛至沓來：“我想申領均勻隨機變量的熵 :)”，London School of Geometry and Number Theory 的博士生 Paul Lezeau 寫道。“我打算嘗試處理一般的纖維化恒等式，”UCLA 的博士生 Aaron Anderson 回復道。

通過口耳相傳，越來越多的數學家加入了這項工作。到 11 月底，陶哲軒就像一位忙碌的志愿者協調員，自己很少再寫 Lean 代碼，而是專注于為他人找任務。11月28日，他寫道：“鑒于在 PFR 項目接近完成時我們可能暫時有志愿者過剩的情況，我想到了一個額外的小任務，也許有人愿意做。”46分鐘后，Kim Morrison 回復說他們已經完成了這項任務。“哇，真快！謝謝！”陶哲軒答道。

甚至在形式化完成之前，Lean 社區就開始討論其意義。他們特別爭論了該項目的效率是否預示著快速形式化的新時代，還是僅僅反映了陶哲軒的獨特影響力。在小組帖子的總結發言中，陶哲軒反思道，他自己并沒有編寫太多代碼。“這實際上讓我很受鼓舞，因為它表明數學家們無需具備高超的 Lean 編程技能，就能牽頭開展Lean形式化項目（當然，至少需要具備陳述引理的能力，即便無法證明它們）。”八分鐘后，Utrecht University 的數學家、Mathlib 計劃的負責人 Johan Commelin 回復道：“我不想馬上搶占這個話題，”接著質疑了陶哲軒在項目中所學到的經驗教訓是否具有普遍適用性。“當然，由于該項目的高知名度，你得到了很多幫助，”他寫道。

Commelin 還指出，盡管像 PFR 這樣的項目參與起來很有趣且令人興奮，但參與這些項目并不為年輕數學家申請學術職位時帶來好處。“目前，尚不清楚形式化者（姑且這么稱呼吧）將如何被數學界認可，以及這些活動在就業市場上將如何被評估。”陶哲軒回答：“不管怎樣，我很樂意在推薦信中酌情提及對這個項目的貢獻。”

到 2024 年，陶哲軒已成為最引人注目的、宣傳機器輔助數學潛力的公眾聲音。他在拜登總統的科學技術顧問委員會任職已進入第三個年頭，并成為了一個關于生成式人工智能的工作組的聯合主席。在 2024 年的兩場高知名度的演講中，他表達了他對一種新型數學合作的愿景：這種合作結合了人類的洞察力、大型語言模型的創造力，以及形式化驗證系統提供的正確性保證。

他之所以得出這個觀點，部分原因是他看到了當前 AI 工具的明顯局限性。它們擅長解決簡單的問題或有大量先前數據的任務，但在數學的前沿——那里已發表成果很少，可用于訓練的數據也很少——AI 就力不從心了。在他早期使用大語言模型的實驗中，他觀察到它們表現得像過于自信的本科生：它們會提出各種建議，但卻沒有足夠的能力來判斷這些建議的好壞。

不過，陶哲軒心中已有前進的方向。他認為 AI 不會很快取代人類數學家，但他確實認為 AI 特別適合幫助解決某些類型的復雜數學問題：那些可以分解為成千上萬個易處理的小型子問題的問題——基本上與適合 Polymath 項目的是同一類問題。在這種規模上，數學家可以使用 AI 來解決大量最簡單的子問題，將其結果輸出為 Lean 可以檢查的形式化證明，然后再介入處理剩余的、最困難的、需要他們自己解決的問題。2024 年，陶哲軒向任何愿意傾聽的人宣傳這一愿景，并且在 PFR 項目之后，他意識到如果他真的相信這項工作，他需要挺身而出，親自領導。他也立刻確定了首先從哪個問題開始。

這是一年前他偶然發現的一個問題。2023 年 7 月，一位 MathOverflow 用戶提出了一個看似簡單的謎題。考慮一個像加法這樣的運算，它可能遵循某些基本的代數定律，如交換

在許多情況下，一個定律與另一個定律之間沒有關系——例如，交換律并不意味著結合律。

這個 MathOverflow 上的問題涉及兩個特定定律之間的關系，另一位用戶迅速回答了它。

但是，關于定律之間如何普遍關聯的問題引起了陶哲軒的好奇心。他沒有一個接一個地解決謎題，而是開始繪制一個粗略的圖表，展示不同可能的代數定律之間如何相互關聯。很明顯，這幅圖景可能非常復雜。

他發現，如果他將研究限制在涉及恰好四次運算的代數法則上，那么需要考慮大約 4,694個定律。每個定律可能蘊含或不蘊含任何其他定律，從而產生了 2200萬個邏輯蘊含關系需要檢查。一旦他檢查了所有關系——要么證明它們成立，要么找到它們不成立的反例——他就能夠全面了解這全部 4,694個定律之間是如何相互關聯的。他認為，這樣的規模正好適合他所提出的這種新數學方式。

陶哲軒將他的新事業稱為“Equational Theories”，并于 2024 年 9 月 25 日在他的個人博客上發帖宣布了該項目的啟動。他開篇逐一列舉了過去大規模公共數學合作之所以困難的主要原因，然后寫道：“像 Lean 這樣的證明輔助語言，提供了一種克服這些障礙的潛在方法。”

起初，陶哲軒和越來越多的加入他的志愿者針對被稱為“原群”（magmas）的簡單數學結構測試了,4,000多個定律。原群是一種簡化版本的算術系統，可以作為一個有用的起點，因為任何對原群不成立的定律都不可能蘊含其他更復雜的定律。參與者們迅速使用基本的 Python 腳本測試了數百萬個這樣的簡化系統，并在幾天內解決了這2200 萬個潛在蘊含關系中的 99%以上。陶哲軒在第二天（9月27日）發帖稱，他對項目進展之快感到驚訝：“這個項目的進展速度遠遠快于我的預期，其規模擴大的速度也遠遠超過我的預期——僅僅48小時，很大一部分蘊含關系很可能很快就能解決！我以為為期三周的 PFR 項目已經很快了，但這個速度簡直瘋狂得離譜。”

一旦最簡單的蘊含關系得到解決，“Equational Theories”的志愿者們以去中心化的方式轉向了自動化定理證明器，這些證明器可以在無需交互式幫助的情況下自行搜索問題的解決方案。這些證明器，加上傳統的人類聰明才智，逐個攻克了懸而未決的問題。

就像一位科學家看著自己的造物變為現實，陶哲軒欣賞著工作的展開。“這個項目似乎正在成功地實現去中心化；特別是，現在有很多活動是我并不完全了解的，”他寫道。

對許多數學家來說，陶哲軒的項目很有趣，但也很奇怪。Buzzard 關注著這個項目，被這個社會實驗所吸引，但對“Equational Theories”的數學內容感到無聊。他認為它既基礎又古怪，不過他還是欽佩陶哲軒的創造力。另一位著名數學家 John Baez 則更直言不諱。他說：“在我看來，這似乎是在巨大地浪費時間，”接著他承認他對大學橄欖球也有同感，而且很多人也喜歡那個。

一個月內，“Equational Theories”小組將 2200萬個問題縮小到238 個。到 11 月下旬，減少到138 個。當他們逐步解決剩余案例時，進展放緩了。新年伊始，大約有 30個蘊含關系仍未解決，進展速度進一步放緩。到 3 月底，他們已在僅存的四個問題上卡了好幾周。參與者們嘗試處理剩余的問題，但由于只剩下這么少的蘊含關系，許多人逐漸離開了；陶哲軒的更新也從近乎每日的頻率減少到每幾周一次。

然而，解決全部2200 萬個蘊含關系中的每一個從來就不是“Equational Theories”的真正目標。出于純粹的好奇心，陶哲軒想要一張完整圖景的地圖，而現在他有了，盡管缺少了一些細節。更重要的是，他將“Equational Theories”視為一種根本性的數學新方式的試點項目——在這方面，它是不折不扣的成功。

在陶哲軒看來，“Equational Theories”是他希望成為“實驗”數學新時代的開端。他心中所想的是那種已經發生在物理學等領域的變革。物理學曾經在很大程度上是一門理論學科，孤獨的思想家或小型合作團隊一次處理一兩個問題——換句話說，它過去看起來很像數學現在的樣子。但隨著技術的進步，該領域出現了一個新的實驗分支——在像 CERN 的大型強子對撞機這樣的實驗室里進行的大規模合作，數百甚至數千名具有專業技能的研究人員共同工作，并生成大量數據。這些實驗并沒有取代理論，而是對其進行了補充，新的研究成果在兩種研究范式間雙向流動、相互促進。

陶哲軒想象著數學界發生類似的演變。他相信，新穎的探究形式將不可避免地帶來新穎的見解，正如過去一貫如此。當“Equational Theories”團隊有條不紊地從他們龐大的表格中劃掉蘊含關系時，他們偶然發現了真正新穎的數學構造——比如“原群上同調”，這是對群上同調概念的一種奇特擴展。群上同調是一個深刻且被廣泛研究的領域，描述了群何時可以或不可以以某種方式被擴展。陶哲軒聯系了 John Baez——這位“Equational Theories”的反對者同時也是上同調專家——詢問這種構造以前是否見過。Baez 承認他從未遇到過。

在陶哲軒看來，這正是關鍵所在。該項目表明，數學可以以不同的、實驗性的方式進行——并且在此過程中，它確實發現了一些真正新穎的東西。陶哲軒從未期望“Equational Theories”能挖掘出什么驚天動地的啟示；他想要的是證明一種新型數學機器的有效性。從這個意義上說，它成功了。陶哲軒找到了一種做數學的新方法，而且他沒有表現出任何要回頭的意思。

下文改編自 Kevin Hartnett 所著的 The Proof in the Code: How a Truth Machine Is Transforming Math and AI。版權所有 ? 2026 Kevin Hartnett。計劃于2026年6月9日由 Quanta Books 與 Farrar, Straus and Giroux 合作出版。保留所有權利。

本文原載微信公眾號“數學家”（校對：慧玲；責編：），原標題：數學領域人工智能的布道者，有修訂。

特 別 提 示

『返樸』提供按月檢索功能。關注公眾號，回復四位數組成的年份+月份，如“1903”，可獲取2019年3月的內容目錄，以此類推。