★置頂zzllrr小樂公眾號(hào)，追蹤《小樂數(shù)學(xué)科普》系列報(bào)道！

借助自動(dòng)化證明校驗(yàn)工具，一道數(shù)學(xué)難題可被拆解為多個(gè)小模塊（chunks），逐一攻克后再整合起來，且能確保每一個(gè)推導(dǎo)環(huán)節(jié)準(zhǔn)確無誤。在部分學(xué)者看來，這預(yù)示著數(shù)學(xué)研究即將邁入全新階段。

諸如Lean這類自動(dòng)化證明校驗(yàn)工具，能夠?yàn)閿?shù)學(xué)證明的嚴(yán)謹(jǐn)性提供絕對(duì)保障。

圖源：Samuel Velasco |《量子雜志》Quanta Magazine

代碼致謝：亞歷克斯?康托羅維奇（Alex Kontorovich）

作者：Kevin Hartnett（凱文?哈特內(nèi)特，量子雜志特約撰稿人）2026-6-8

譯者：zzllrr小樂（數(shù)學(xué)科普公眾號(hào)）2026-6-9

求喜歡

引言

凱文?哈特內(nèi)特（ Kevin Hartnett ）

本文節(jié)選自凱文?哈特內(nèi)特（Kevin Hartnett）2026年6月新書《代碼中的證明：一臺(tái)真理機(jī)器如何重塑數(shù)學(xué)與AI人工智能》The Proof in the Code: How a Truth Machine Is Transforming Math and AI。

陶哲軒向來樂于接納非主流的全新理念。2014年11月，他與另外四位杰出數(shù)學(xué)家共同出席座談，五人均為首屆數(shù)學(xué)突破獎(jiǎng)得主，該獎(jiǎng)項(xiàng)獎(jiǎng)金高達(dá) 300 萬美元。座談期間，眾人探討了諸多話題：數(shù)學(xué)究竟是人類的創(chuàng)造，還是原本就存在的客觀發(fā)現(xiàn)？多數(shù)數(shù)學(xué)家認(rèn)為，至少在研究過程中，數(shù)學(xué)更像是一種 “發(fā)現(xiàn)”；眾人還聊到人類或許活在數(shù)字虛擬世界中的可能性。馬克西姆?孔采維奇（Maxim Kontsevich）是1990年代深耕數(shù)學(xué)與物理交叉領(lǐng)域的頂尖學(xué)者，他直言：“我認(rèn)為我們當(dāng)下所處的世界并非真實(shí)。”

但在這場長達(dá) 40 分鐘的交流中，最讓眾人難以置信的言論，均出自陶哲軒之口。他預(yù)言，未來數(shù)學(xué)家將不再獨(dú)自鉆研，或是僅與兩三位同行組成小團(tuán)隊(duì)開展研究，而是會(huì)和數(shù)百名研究者協(xié)作攻克課題。他還以一貫謙遜平和的語氣補(bǔ)充道：這類大型協(xié)作項(xiàng)目完成后，研究成果也不再由人類審稿人核驗(yàn)，而是交由計(jì)算機(jī)完成?！敖K有一天，我們撰寫學(xué)術(shù)論文將不再使用 LaTeX 排版語言，而是借助專用軟件將文稿轉(zhuǎn)化為形式化語言。編寫過程中還會(huì)頻繁出現(xiàn)編譯報(bào)錯(cuò) —— 這意味著計(jì)算機(jī)無法理解某一步推導(dǎo)邏輯?！?/p>

這番言論一出，現(xiàn)場主持人與其他獲獎(jiǎng)?wù)呒娂娪X得荒誕不經(jīng)，相比之下，“人類活在虛擬世界” 的猜想反倒顯得合情合理。陶哲軒提出大規(guī)模協(xié)作模式，本身就格外出人意料，因?yàn)槭廊搜壑?，他本就是最擅長獨(dú)自深耕研究的數(shù)學(xué)家。

陶哲軒 1975 年出生于澳大利亞阿德萊德（Adelaide），他的父母三年前從中國香港移民至此。陶哲軒的過人天賦在幼年時(shí)期便展露無遺。兩歲時(shí)，父母帶他拜訪友人，發(fā)現(xiàn)他正和幾名六歲的孩子圍坐在一起，用積木教大家數(shù)數(shù)。當(dāng)被問及從何處學(xué)會(huì)數(shù)數(shù)時(shí)，他回答是從《芝麻街》Sesame Street節(jié)目里學(xué)到的。七歲那年，他開始系統(tǒng)學(xué)習(xí)微積分。

《代碼中的證明》一書，探尋人機(jī)協(xié)作開展數(shù)學(xué)研究的新時(shí)代。

圖源：Samuel Velasco / Quanta Magazine

1985年春天，陶哲軒的父母帶著他遠(yuǎn)赴美國，拜訪了約翰斯?霍普金斯大學(xué) “數(shù)學(xué)天賦青少年研究項(xiàng)目” 負(fù)責(zé)人朱利安?斯坦利（Julian Stanley）。斯坦利評(píng)價(jià)，陶哲軒是他畢生見過數(shù)學(xué)天賦最高的孩子。同年，著名數(shù)學(xué)家保羅?埃爾德什（Paul Erd?s）到訪阿德萊德，二人得以相遇。一張經(jīng)典照片記錄下當(dāng)時(shí)的場景：彼時(shí) 72 歲、須發(fā)花白的埃爾德什低頭看著手中文稿，年僅十歲的陶哲軒站在一旁，黑發(fā)濃密，手托下巴，全神貫注地凝視文稿，陷入沉思。

彼時(shí)72歲的保羅?埃爾德什，與年僅十歲的陶哲軒同框。

圖源：Billy Grace Tao

陶哲軒的傳奇少年之路仍在延續(xù)。1986年，他首次參加IMO國際數(shù)學(xué)奧林匹克競賽，斬獲銅牌，成為該賽事史上最年輕的銅牌得主。此后兩年，他接連刷新紀(jì)錄，先后成為史上最年輕的銀牌、金牌獲得者。他的求學(xué)之路同樣一路高歌猛進(jìn)：15歲便從阿德萊德的弗林德斯大學(xué)畢業(yè)；1992年秋季，他隨父親前往美國新澤西州，進(jìn)入普林斯頓大學(xué)攻讀數(shù)學(xué)博士學(xué)位。埃爾德什曾專門為他撰寫推薦信，助力其破格入學(xué)，信中寫道：“我堅(jiān)信，他必將成長為一流數(shù)學(xué)家，甚至有望躋身偉大數(shù)學(xué)家之列。”

埃爾德什的預(yù)判最終成真。24 歲時(shí)，陶哲軒已憑借多項(xiàng)重磅研究成果，手握多所頂尖高校的終身教職邀約，最終他選擇執(zhí)教于加州大學(xué)洛杉磯分校。也正是在這一時(shí)期，他結(jié)識(shí)了英國頂尖數(shù)論學(xué)家本?格林（Ben Green）。二人攜手開展一項(xiàng)重要證明：即便素?cái)?shù)在數(shù)軸上看似隨機(jī)分布，海量素?cái)?shù)集合中也必然存在特定規(guī)律的等差數(shù)列（例如 7、10、13、16，相鄰數(shù)字差值恒定）。這項(xiàng)成果成為陶哲軒早年職業(yè)生涯的代表作，助力他在2006年斬獲菲爾茲獎(jiǎng)，也讓他穩(wěn)居全球頂尖數(shù)學(xué)家行列。

即便孤身一人也能成就一番事業(yè)，陶哲軒卻始終偏愛協(xié)作研究。在他看來，與同行交流合作是迸發(fā)新思想的核心途徑 —— 將彼此的知識(shí)融會(huì)貫通，便能催生全新發(fā)現(xiàn)。

這種研究思路，讓陶哲軒的研究版圖變得極為廣闊：從解析數(shù)論（代表作即與格林合作的格林-陶定理），到分析學(xué)（研究描述流體運(yùn)動(dòng)的納維-斯托克斯方程），再到基于數(shù)字?jǐn)?shù)據(jù)重構(gòu)核磁共振影像的算法。其中，核磁共振相關(guān)研究的緣起十分有趣：當(dāng)時(shí)他與加州理工學(xué)院的統(tǒng)計(jì)學(xué)家埃馬紐埃爾?坎德什（Emmanuel Candès）在幼兒園接送孩子，二人閑聊間萌生了合作想法。樂于協(xié)作、樂于公開分享研究的特質(zhì)，促使陶哲軒在 2007 年開設(shè)了個(gè)人博客 https://terrytao.wordpress.com ，定期更新研究進(jìn)展。彼時(shí)的他，早已是全球家喻戶曉的頂尖數(shù)學(xué)家。博客文章吸引了大量讀者，評(píng)論區(qū)常常掀起熱烈的學(xué)術(shù)討論，陶哲軒也會(huì)積極參與互動(dòng)。他坦言，一方面是享受交流的樂趣，另一方面也希望在思想碰撞中收獲新靈感。

同期，另一位知名數(shù)學(xué)家蒂莫西?高爾斯（Timothy Gowers，也是菲爾茲獎(jiǎng)得主，譯者注）也熱衷線上學(xué)術(shù)交流。但他并不滿足于博客評(píng)論區(qū)零散的靈感碰撞，而是希望組織有目標(biāo)的大規(guī)模公開協(xié)作。2009年1月，高爾斯在博客發(fā)文，提出打造一種全新的 “大規(guī)模協(xié)作數(shù)學(xué)研究模式”：在公開線上論壇拋出數(shù)學(xué)難題，歡迎所有感興趣的人建言獻(xiàn)策。這一項(xiàng)目被命名為博學(xué)者計(jì)劃（Polymath Project，Polymath既有博學(xué)者之意，又有多種（Poly）數(shù)學(xué)（Math）之意，雙關(guān)，譯者注）。

陶哲軒第一時(shí)間加入其中。他和高爾斯都清楚，并非所有數(shù)學(xué)難題都適合大規(guī)模協(xié)作，適合協(xié)作的難題需滿足一個(gè)核心條件：能夠拆解為大量可并行推進(jìn)的子問題。將主難題拆分為多個(gè)獨(dú)立小問題后，不同團(tuán)隊(duì)、不同研究者便可分頭攻關(guān)，最終整合所有成果，拼湊出完整答案。但陶哲軒也預(yù)判到，博學(xué)者模式最大的挑戰(zhàn)在于統(tǒng)籌管理：既要梳理整合各方觀點(diǎn)，還要逐一核驗(yàn)所有推導(dǎo)內(nèi)容的正確性。

博學(xué)者計(jì)劃首個(gè)研究課題，是優(yōu)化黑爾斯-朱厄特（Hales-Jewett）定理（該定理研究用兩種顏色為網(wǎng)格單元格涂色時(shí)產(chǎn)生的規(guī)律）。數(shù)十位數(shù)學(xué)家在論壇留下數(shù)千條討論內(nèi)容，歷經(jīng)數(shù)月協(xié)作，團(tuán)隊(duì)成功推導(dǎo)出該涂色規(guī)律更精準(zhǔn)的結(jié)論。同年秋季，團(tuán)隊(duì)以聯(lián)合筆名 “D.H.J. 博學(xué)者” （D.H.J. Polymath）發(fā)布論文，這也是史上首篇依托大規(guī)模公開協(xié)作完成的數(shù)學(xué)論文。高爾斯的嘗試大獲成功，專業(yè)數(shù)學(xué)家與數(shù)學(xué)愛好者攜手，順利完成了一項(xiàng)數(shù)學(xué)證明。

此后十年間，博學(xué)者計(jì)劃陸續(xù)開展了 15 個(gè)課題，其中部分由陶哲軒牽頭，該項(xiàng)目也逐漸受到主流媒體關(guān)注。2011年10月29日，《華爾街日報(bào)》刊發(fā)題為《新一代愛因斯坦，必將是樂于分享的科學(xué)家》The New Einsteins Will Be Scientists Who Share的報(bào)道，稱博學(xué)者計(jì)劃開創(chuàng)了全新的解題范式。

證明輔助工具解析

證明輔助工具 Lean 能夠協(xié)助數(shù)學(xué)家完成定理證明：既校驗(yàn)推導(dǎo)過程，也可自動(dòng)完成部分證明步驟。

1. 數(shù)學(xué)庫（Mathlib）

   以 Lean 語言編寫的數(shù)學(xué)知識(shí)庫，全球數(shù)學(xué)家持續(xù)為其補(bǔ)充內(nèi)容。數(shù)學(xué)家搭建證明整體框架，梳理推導(dǎo)步驟。

3. 指令集（Tactics，策略集）

   數(shù)學(xué)庫中內(nèi)置各類程序指令，可自動(dòng)執(zhí)行證明步驟；經(jīng)過校驗(yàn)的定理會(huì)同步錄入數(shù)學(xué)庫。

5. 核心內(nèi)核（Kernel）

   依靠固定規(guī)則逐行核驗(yàn)證明邏輯的正確性。

Lean 社群中，章魚表情逐漸成為大家表達(dá)喜悅的專屬符號(hào)。

盡管博學(xué)者計(jì)劃取得了開創(chuàng)性成果，但在陶哲軒看來，這一模式仍存在時(shí)代局限性。大規(guī)模協(xié)作帶來思維碰撞的同時(shí)，出錯(cuò)概率也大幅提升，所有內(nèi)容都需要專人逐一人工核驗(yàn)，審核環(huán)節(jié)成為整個(gè)項(xiàng)目的瓶頸，也讓博學(xué)者計(jì)劃難以長久運(yùn)轉(zhuǎn)。

陶哲軒真正追求的，是一套高效的全新科學(xué)研究模式。他意識(shí)到，單純依靠論壇協(xié)作遠(yuǎn)遠(yuǎn)不夠，想要實(shí)現(xiàn)理想，必須借助計(jì)算機(jī)自動(dòng)核驗(yàn)成果，替代低效的人工審核。但在2010年代，這項(xiàng)技術(shù)尚不成熟，實(shí)現(xiàn)難度堪比載人登陸火星。

陶哲軒多年來一直關(guān)注計(jì)算機(jī)形式化數(shù)學(xué)證明領(lǐng)域，也知曉該領(lǐng)域?yàn)閿?shù)不多的成功案例。但他同樣清楚，彼時(shí)的形式化數(shù)學(xué)工具實(shí)操性極差，多數(shù)場景下，投入的時(shí)間與精力遠(yuǎn)大于實(shí)際收益。即便如此，他依舊看好這項(xiàng)技術(shù)的潛力。在全球頂尖數(shù)學(xué)家群體中，陶哲軒是少數(shù)主動(dòng)擁抱新型數(shù)學(xué)研究工具的學(xué)者。

2022年7月，為深入了解計(jì)算機(jī)在數(shù)學(xué)研究中的應(yīng)用，陶哲軒牽頭組織了一場專題研討會(huì)，并邀請凱文?巴扎德（Kevin Buzzard）擔(dān)任聯(lián)合組織者 —— 巴扎德是當(dāng)時(shí)全球推廣形式化數(shù)學(xué)最具影響力的學(xué)者。

詳情參閱：

參會(huì)之初，陶哲軒認(rèn)為 Lean 是一套復(fù)雜的工具，至少需要數(shù)月時(shí)間才能上手。但在巴扎德的鼓勵(lì)下，他決定親自嘗試。同時(shí)，他也認(rèn)為自己應(yīng)當(dāng)以身作則：既然致力于推廣計(jì)算機(jī)輔助證明，就必須親身實(shí)踐。

2023年10月9日，陶哲軒在社交平臺(tái)發(fā)文：“我決定正式學(xué)習(xí)交互式證明系統(tǒng) Lean4，過程中也會(huì)借助人工智能輔助操作。”

隨后，他在數(shù)學(xué)領(lǐng)域知名問答平臺(tái) MathOverflow 上，挑選了一道關(guān)于麥克勞林（Maclaurin）不等式的問題，嘗試用 Lean 完成形式化證明，以此作為實(shí)操練習(xí)。他先按照傳統(tǒng)學(xué)術(shù)規(guī)范，手寫了一份共計(jì) 10 頁的標(biāo)準(zhǔn)證明文稿，隨后著手將這份證明轉(zhuǎn)化為 Lean 形式化代碼。

起初，陶哲軒預(yù)估一周就能完成任務(wù)，但很快便發(fā)現(xiàn)手寫數(shù)學(xué)證明與編寫 Lean 代碼存在巨大差異。他感慨道：證明中最難的推導(dǎo)環(huán)節(jié)，在 Lean 中反而容易實(shí)現(xiàn)；而那些看似淺顯直白的結(jié)論，轉(zhuǎn)化為代碼時(shí)卻要耗費(fèi)大量精力。

舉個(gè)簡單例子：傳統(tǒng)數(shù)學(xué)證明中，若已知三個(gè)數(shù)字均大于 1，便可直接得出 “三數(shù)之和不小于 3” 的結(jié)論，無需額外解釋。但 Lean 不接受無依據(jù)的主觀斷言，陶哲軒不得不花費(fèi)時(shí)間，在數(shù)學(xué)庫（Mathlib）中查找對(duì)應(yīng)的引理，以此佐證這個(gè)顯而易見的結(jié)論。此外，傳統(tǒng)數(shù)學(xué)書寫無需嚴(yán)格界定數(shù)域，數(shù)字 “3” 既可以是自然數(shù)，也可以是整數(shù)、實(shí)數(shù)，無需特意區(qū)分。但在 Lean 中，每一個(gè)數(shù)字都必須明確所屬數(shù)域。由于多處遺漏數(shù)域標(biāo)注，他的代碼反復(fù)編譯失敗。

耗時(shí)近一個(gè)月后，2023年11月6日，陶哲軒終于在博客評(píng)論區(qū)宣布：“我已成功將這篇論文的證明內(nèi)容完整轉(zhuǎn)化為 Lean4 形式化代碼。” 盡管這份代碼的編寫質(zhì)量并不理想，但他正式成為 Lean 社群的一員。

學(xué)習(xí) Lean 的同時(shí)，陶哲軒依舊推進(jìn)著多項(xiàng)常規(guī)研究課題。其中一項(xiàng)合作項(xiàng)目，搭檔包括多年好友本?格林、蒂莫西?高爾斯，以及格林的學(xué)生、現(xiàn)任加州大學(xué)圣地亞哥分校教授弗雷迪?曼納斯（Freddie Manners）。這是一支實(shí)力頂尖的團(tuán)隊(duì)：高爾斯與陶哲軒同為菲爾茲獎(jiǎng)得主，格林也是數(shù)論領(lǐng)域的權(quán)威學(xué)者。

四人的研究目標(biāo)聚焦于和集（sumset）這一數(shù)學(xué)概念。簡單來說，給定一組數(shù)字，將集合中每一對(duì)不同數(shù)字相加，所有求和結(jié)果構(gòu)成的新集合，就是原集合的和集。

如果原始集合內(nèi)的數(shù)字雜亂無章，其和集的規(guī)模會(huì)十分龐大。例如 10 個(gè)隨機(jī)數(shù)字，對(duì)應(yīng)的和集約包含 50 個(gè)數(shù)字；1000 個(gè)隨機(jī)數(shù)字，和集數(shù)量可達(dá) 50 萬個(gè)。但如果原始集合具備規(guī)律，和集規(guī)模會(huì)大幅縮小 —— 因?yàn)榇罅壳蠛徒Y(jié)果會(huì)重復(fù)出現(xiàn)，而和集僅保留不重復(fù)的數(shù)值。比如數(shù)字 1 至 10 構(gòu)成的集合（典型的等差數(shù)列），其和集僅包含 17 個(gè)數(shù)字，遠(yuǎn)少于隨機(jī)集合的 50 個(gè)。

1960年代，計(jì)算機(jī)科學(xué)家卡塔琳?馬頓（Katalin Marton）提出一項(xiàng)猜想：若一個(gè)數(shù)字集合的和集規(guī)模極小，那么該集合中必然存在長等差數(shù)列。21 世紀(jì)初，陶哲軒、高爾斯與格林曾針對(duì)該猜想的優(yōu)化版本 ——多項(xiàng)式弗賴曼 - 魯扎（Freiman-Ruzsa）猜想（PFR猜想）開展研究，后續(xù)研究陷入停滯。2023年，陶哲軒、格林與曼納斯重啟該課題，計(jì)劃結(jié)合曼納斯深耕的概率論方法推進(jìn)證明。

三人意識(shí)到，將這套概率論技巧與高爾斯過往的研究思路相結(jié)合，或許就能徹底破解該猜想。于是高爾斯也加入?yún)f(xié)作團(tuán)隊(duì)。2023年整個(gè)夏季，四人穩(wěn)步推進(jìn)研究，深秋時(shí)分終于完成完整證明。（詳情參閱：）11月9日，也就是陶哲軒將首份 Lean 形式化代碼上傳至代碼托管平臺(tái) GitHub 的三天后，四人聯(lián)合論文正式發(fā)布在arXiv學(xué)術(shù)預(yù)印本平臺(tái) https://arxiv.org/abs/2311.05762 。

深耕 Lean 的陶哲軒順勢提議：團(tuán)隊(duì)可以嘗試將這篇重磅論文完整形式化。這篇論文難度適中、影響力深遠(yuǎn)，且論文用到的基礎(chǔ)定義大多已收錄在 Mathlib 中，無需額外搭建底層內(nèi)容，十分適合轉(zhuǎn)化為 Lean 代碼。

但格林、高爾斯與曼納斯都不愿花費(fèi)時(shí)間學(xué)習(xí) Lean。于是陶哲軒決定獨(dú)自牽頭推進(jìn)這項(xiàng)工作，他也預(yù)料到，以自己的影響力，很快會(huì)吸引眾多志愿者加入。

2023年11月13日，陶哲軒在 Lean 專屬交流群新建討論頻道并發(fā)文：“大家好，我計(jì)劃啟動(dòng)一項(xiàng)項(xiàng)目，將我、高爾斯、格林、曼納斯聯(lián)合完成的多項(xiàng)式弗賴曼-魯扎（PFR）猜想證明，完整轉(zhuǎn)化為 Lean4 形式化代碼。我會(huì)借助這個(gè)頻道統(tǒng)籌進(jìn)度，歡迎所有愿意參與的志愿者加入?！?/p>

這是博學(xué)者計(jì)劃的全新升級(jí)版本：不再從零攻克新難題，而是對(duì)已有成熟證明進(jìn)行形式化轉(zhuǎn)化；全程由 Lean 自動(dòng)核驗(yàn)內(nèi)容正確性，徹底擺脫人工審核的負(fù)擔(dān)。

消息發(fā)出次日，斯德哥爾摩大學(xué)博士生雅埃爾?迪利耶斯（Ya?l Dillies）便為項(xiàng)目搭建整體框架，將整份證明拆解為 13 個(gè)模塊。陶哲軒進(jìn)一步細(xì)化任務(wù)，把每個(gè)模塊拆分為多條引理與基礎(chǔ)定義。傳統(tǒng)數(shù)學(xué)論文中，一條輔助證明的引理通常長達(dá) 20 行，而此次項(xiàng)目中，他將引理壓縮至 5 行，最大限度拆分任務(wù)，方便更多人分頭貢獻(xiàn)力量。

項(xiàng)目啟動(dòng)首周，志愿者們主要負(fù)責(zé)補(bǔ)充 Mathlib 中缺失的概率論基礎(chǔ)內(nèi)容，核心任務(wù)是完成香農(nóng)熵（Shannon entropy，用于衡量數(shù)字集合等數(shù)據(jù)的無序程度與不確定性）的形式化定義。與此同時(shí)，團(tuán)隊(duì)也在摸索全新的協(xié)作模式。初期交流延續(xù)了博學(xué)者計(jì)劃的自由討論形式，陶哲軒梳理待辦任務(wù)，眾人自由建言獻(xiàn)策。

11月22日，陶哲軒整理出 22 條待完成引理并發(fā)布：“大家可以自愿認(rèn)領(lǐng)任意引理，在評(píng)論區(qū)留言即可?！?消息一出，報(bào)名者絡(luò)繹不絕。倫敦幾何與數(shù)論研究所博士生保羅?勒佐（Paul Lezeau）留言：“我認(rèn)領(lǐng)均勻隨機(jī)變量的熵相關(guān)引理。” 加州大學(xué)洛杉磯分校博士生艾倫?安德森（Aaron Anderson）則表示，愿意攻克一般纖維恒等式相關(guān)內(nèi)容。

口口相傳之下，越來越多數(shù)學(xué)家加入項(xiàng)目。11月底，陶哲軒幾乎不再親自編寫代碼，主要負(fù)責(zé)統(tǒng)籌分配任務(wù)。11月28日，他發(fā)文表示：“目前項(xiàng)目臨近收尾，志愿者人手充足，我新增一項(xiàng)小任務(wù)，歡迎大家認(rèn)領(lǐng)。”46 分鐘后，學(xué)者金?莫里森（Kim Morrison）便反饋任務(wù)完成。陶哲軒驚嘆道：“速度太快了！非常感謝！”

項(xiàng)目尚未收尾，Lean 社群便開始探討其深遠(yuǎn)意義：有人認(rèn)為，項(xiàng)目的高效推進(jìn)，標(biāo)志著數(shù)學(xué)證明形式化進(jìn)入高速發(fā)展時(shí)代；也有人認(rèn)為，這份成功主要依托陶哲軒的個(gè)人影響力。項(xiàng)目收尾階段，陶哲軒總結(jié)道：“我本人編寫的代碼并不多。這也印證了一件事：數(shù)學(xué)家即便不精通 Lean 編程，只要能夠清晰梳理引理、搭建證明框架，同樣可以牽頭開展形式化項(xiàng)目?！?/p>

烏得勒支大學(xué)數(shù)學(xué)家、Mathlib 項(xiàng)目負(fù)責(zé)人約翰?科梅林（Johan Commelin）隨即留言，提出理性思考：“這個(gè)PFR項(xiàng)目的成功具備特殊性，很難直接復(fù)刻。正因課題關(guān)注度極高，才吸引了大量頂尖志愿者參與?！?他還指出了行業(yè)現(xiàn)實(shí)困境：在當(dāng)前學(xué)術(shù)評(píng)價(jià)體系下，參與證明形式化項(xiàng)目，并不會(huì)成為青年學(xué)者求職、評(píng)職稱的加分項(xiàng)?！皵?shù)學(xué)界目前尚未明確形式化研究者的學(xué)術(shù)定位，這類工作在就業(yè)市場中也難以獲得認(rèn)可。” 對(duì)此，陶哲軒回應(yīng)：“今后為相關(guān)學(xué)者撰寫推薦信時(shí)，我會(huì)主動(dòng)提及他們在本項(xiàng)目中的貢獻(xiàn)?！?/p>

2024年，陶哲軒已然成為推廣機(jī)器輔助數(shù)學(xué)的核心發(fā)聲者。彼時(shí)，他已在美國總統(tǒng)科學(xué)技術(shù)顧問委員會(huì)任職三年，并擔(dān)任生成式人工智能專項(xiàng)工作組聯(lián)合主席。在2024年多場重要演講中，他描繪了新一代數(shù)學(xué)協(xié)作模式：融合人類的原創(chuàng)思維、大語言模型的算力優(yōu)勢，以及形式化核驗(yàn)系統(tǒng)的嚴(yán)謹(jǐn)保障。

這份構(gòu)想，源于他對(duì)當(dāng)下人工智能能力的清醒認(rèn)知?，F(xiàn)有人工智能擅長解決數(shù)據(jù)充足、思路明確的常規(guī)問題，但面對(duì)數(shù)學(xué)前沿領(lǐng)域 —— 這類領(lǐng)域缺乏海量公開研究成果、難以搭建訓(xùn)練數(shù)據(jù)集，人工智能便會(huì)力不從心。在測試大語言模型的過程中，陶哲軒發(fā)現(xiàn)，這類工具就像過度自信的本科生：能夠主動(dòng)給出解題思路，卻無法分辨觀點(diǎn)的優(yōu)劣對(duì)錯(cuò)。

但陶哲軒依舊找到了人工智能與數(shù)學(xué)結(jié)合的可行路徑。他認(rèn)為，人工智能短期內(nèi)絕不會(huì)取代人類數(shù)學(xué)家，卻十分適合拆解大型復(fù)雜數(shù)學(xué)難題：將主問題拆分為數(shù)千個(gè)簡單子問題（這與博學(xué)者計(jì)劃的思路不謀而合）。人工智能可批量攻克難度最低的子問題，并輸出經(jīng)過 Lean 核驗(yàn)的標(biāo)準(zhǔn)形式化證明；而人類數(shù)學(xué)家則聚焦攻克剩余的核心難題。2024年，陶哲軒四處宣講這套研究模式。在多項(xiàng)式弗賴曼-魯扎（PFR）猜想形式化項(xiàng)目成功后，他決定親自牽頭，落地這套全新研究體系，而他選定的首個(gè)課題，源自2023年偶然看到的一道趣味問題。

2023年7月，MathOverflow 上一名用戶提出一道看似簡單的謎題：以加法運(yùn)算為例，加法滿足交換律（x+y=y+x）、結(jié)合律（(x+y)+z=x+(y+z)）等基礎(chǔ)代數(shù)法則。多數(shù)情況下，不同法則之間相互獨(dú)立 —— 比如交換律無法推導(dǎo)出結(jié)合律。

這道謎題探討兩條特定代數(shù)法則之間的邏輯關(guān)系，很快便有網(wǎng)友給出解答。但各類代數(shù)法則之間的內(nèi)在關(guān)聯(lián)，深深勾起了陶哲軒的好奇心。他不再局限于解答零散謎題，而是著手梳理一張圖譜，梳理所有代數(shù)法則之間的推導(dǎo)關(guān)系。梳理過程中他發(fā)現(xiàn)，這套邏輯體系遠(yuǎn)比想象中復(fù)雜。

他劃定研究范圍：僅分析運(yùn)算次數(shù)恰好為四次的代數(shù)法則。經(jīng)統(tǒng)計(jì)，這類法則共計(jì) 4694 條。任意兩條法則之間，都存在 “能否相互推導(dǎo)” 的邏輯關(guān)系，總計(jì)需要驗(yàn)證 2200 萬組邏輯推導(dǎo)。逐一完成所有驗(yàn)證（要么證明推導(dǎo)成立，要么舉出反例推翻推導(dǎo)）后，就能完整厘清這 4694 條法則的全部關(guān)聯(lián)。在陶哲軒看來，這個(gè)課題的規(guī)模，完美適配他構(gòu)想的新一代數(shù)學(xué)研究模式。

陶哲軒將這個(gè)全新項(xiàng)目命名為等式理論（Equational Theories） https://teorth.github.io/equational_theories/，并于2024年9月25日在個(gè)人博客正式官宣。開篇他總結(jié)了傳統(tǒng)大規(guī)模公開數(shù)學(xué)協(xié)作模式的諸多弊端，并直言：“Lean 這類證明輔助語言，有望徹底破解這些難題?！?/p>

項(xiàng)目啟動(dòng)后，陶哲軒與大批志愿者率先借助泛代數(shù)結(jié)構(gòu)——原群（magma）開展測試。原群是簡化版的算術(shù)結(jié)構(gòu)，十分適合作為研究起點(diǎn)：若某條法則在原群中不成立，便不可能推導(dǎo)出其他更復(fù)雜的法則。志愿者們運(yùn)用基礎(chǔ) Python 腳本，批量測試海量法則。短短數(shù)日，2200 萬組邏輯推導(dǎo)中，超過 99% 都得到驗(yàn)證。

項(xiàng)目啟動(dòng)第二天（9月27日），陶哲軒發(fā)文感慨進(jìn)度遠(yuǎn)超預(yù)期：“項(xiàng)目推進(jìn)速度、協(xié)作規(guī)模都大大超出我的想象。僅僅 48 小時(shí)，絕大部分邏輯推導(dǎo)即將完成驗(yàn)證。此前為期三周的多項(xiàng)式弗賴曼-魯扎猜想項(xiàng)目已算高效，而本次項(xiàng)目的推進(jìn)速度更是創(chuàng)下新高。”

基礎(chǔ)推導(dǎo)驗(yàn)證完畢后，志愿者們借助全自動(dòng)定理證明器，結(jié)合人工推導(dǎo)，逐一攻克剩余難題。整個(gè)項(xiàng)目逐漸走向去中心化運(yùn)轉(zhuǎn)，許多研究進(jìn)展甚至不再經(jīng)過陶哲軒統(tǒng)籌。他對(duì)此評(píng)價(jià)道：“項(xiàng)目已實(shí)現(xiàn)自主運(yùn)轉(zhuǎn)，不少研究工作我都未能實(shí)時(shí)跟進(jìn)，這正是我希望看到的狀態(tài)?！?/p>

部分?jǐn)?shù)學(xué)家認(rèn)為這個(gè)課題新奇卻略顯冷門。全程關(guān)注項(xiàng)目進(jìn)展的巴扎德表示，這是一場有趣的社會(huì)實(shí)驗(yàn)，只是課題本身的數(shù)學(xué)內(nèi)容較為基礎(chǔ)、風(fēng)格另類，但他十分認(rèn)可陶哲軒的創(chuàng)新思路。知名數(shù)學(xué)家約翰?貝茲（John Baez）則直言：“在我看來，這項(xiàng)工作純粹是浪費(fèi)時(shí)間?！?隨后他又補(bǔ)充道，自己也曾用同樣的看法看待大學(xué)橄欖球，但依舊有無數(shù)人樂在其中。

項(xiàng)目推進(jìn)一個(gè)月后，2200 萬組待驗(yàn)證邏輯推導(dǎo)僅剩 238 組；11月末，剩余數(shù)量縮減至 138 組。隨著難題難度逐步提升，進(jìn)度明顯放緩。2025年伊始，僅剩下 30 組推導(dǎo)懸而未決，推進(jìn)速度進(jìn)一步下降。截至2025年3月底，團(tuán)隊(duì)卡在最后4組推導(dǎo)上，停滯數(shù)周。剩余難題過少，大量志愿者陸續(xù)退出，陶哲軒的項(xiàng)目更新頻率也從每日播報(bào)，變?yōu)閿?shù)周一更。

不過，徹底攻克全部 2200 萬組推導(dǎo)，本就不是 “等式理論” 項(xiàng)目的核心目標(biāo)。陶哲軒最初只是出于好奇，想要繪制出完整的代數(shù)法則關(guān)聯(lián)圖譜，如今除少數(shù)細(xì)節(jié)外，核心目標(biāo)已然實(shí)現(xiàn)。更重要的是，在他眼中，這個(gè)項(xiàng)目是實(shí)驗(yàn)性數(shù)學(xué)新時(shí)代的試點(diǎn)工程，而這場試點(diǎn)無疑大獲成功。（詳情參閱

陶哲軒認(rèn)為，“等式理論” 項(xiàng)目拉開了實(shí)驗(yàn)性數(shù)學(xué)時(shí)代的序幕。他以物理學(xué)的發(fā)展歷程類比數(shù)學(xué)：物理學(xué)也曾以理論研究為主，依靠獨(dú)立學(xué)者或小型團(tuán)隊(duì)逐一攻克難題，和如今的數(shù)學(xué)研究模式高度相似。但隨著技術(shù)革新，實(shí)驗(yàn)物理應(yīng)運(yùn)而生。歐洲核子研究中心的大型強(qiáng)子對(duì)撞機(jī)等大型實(shí)驗(yàn)裝置，匯聚數(shù)百乃至數(shù)千名專業(yè)研究者協(xié)同作業(yè)，產(chǎn)出海量實(shí)驗(yàn)數(shù)據(jù)。實(shí)驗(yàn)物理并未取代理論物理，而是與之相輔相成，兩類研究成果相互啟發(fā)、彼此推進(jìn)。

陶哲軒堅(jiān)信，數(shù)學(xué)也將迎來同樣的變革。全新的研究模式，必然會(huì)催生全新的數(shù)學(xué)發(fā)現(xiàn)。在志愿者逐條驗(yàn)證海量邏輯推導(dǎo)的過程中，團(tuán)隊(duì)意外發(fā)現(xiàn)了全新的數(shù)學(xué)概念 ——原群上同調(diào)。這一概念是群上同調(diào)的全新延伸，而群上同調(diào)是數(shù)學(xué)界研究已久的經(jīng)典領(lǐng)域，主要探究群結(jié)構(gòu)的拓展規(guī)律。陶哲軒特意請教該領(lǐng)域權(quán)威學(xué)者、此前并不看好項(xiàng)目的約翰?貝茲，對(duì)方坦言，從未見過這類全新構(gòu)造。

這正是陶哲軒打造新項(xiàng)目的初衷。他并未指望 “等式理論” 能誕生顛覆性數(shù)學(xué)結(jié)論，而是希望借此驗(yàn)證一套全新數(shù)學(xué)研究體系的可行性。從這個(gè)角度來看，項(xiàng)目圓滿達(dá)成目標(biāo)。陶哲軒成功探索出數(shù)學(xué)研究的全新路徑，而他也堅(jiān)定地選擇沿著這條新路繼續(xù)前行。

本文節(jié)選自凱文?哈特內(nèi)特著作《代碼中的證明：一臺(tái)真理機(jī)器如何重塑數(shù)學(xué)與AI人工智能》。該書由《量子圖書》Quanta Books聯(lián)合法勒（Farrar）、斯特勞斯（Straus）和吉魯（Giroux）出版社出版，定于2026年6月9日正式發(fā)行，版權(quán)所有。

參考資料

https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/

小樂數(shù)學(xué)科普近期文章

小樂數(shù)學(xué)科普歷年合集

版權(quán)聲明：本文首發(fā)于微信公眾號(hào)“zzllrr小樂”的專欄《小樂數(shù)學(xué)科普》。歡迎個(gè)人轉(zhuǎn)發(fā)。如需轉(zhuǎn)載，請?jiān)凇皕zllrr小樂”公眾號(hào)后臺(tái)回復(fù)“轉(zhuǎn)載”，還可通過公眾號(hào)菜單、發(fā)送郵件到zzllrr@gmail.com與我們?nèi)〉寐?lián)系。相關(guān)圖文音視頻內(nèi)容默認(rèn)遵守CC BY-NC 4.0知識(shí)共享協(xié)議，未獲作者和譯者授權(quán)，禁止用于營銷宣傳和商業(yè)目的。

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評(píng)論、點(diǎn)贊、在看、在聽

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點(diǎn)擊底部一起捐

助力騰訊公益

點(diǎn)擊zzllrr小樂

公眾號(hào)主頁

右上角

置頂★加星

數(shù)學(xué)科普不迷路！