菲爾茲獎得主也要學寫程式：陶哲軒與重塑數學的「真理機器」

一個程式，讓數學家不再需要「相信」彼此的證明是對的，而是能「知道」。

這不是科幻小說的情節。Quanta Magazine 資深記者 Kevin Hartnett 在六月初出版的新書《The Proof in the Code》裡，記錄了一個出乎所有人意料的故事：微軟研究院的巴西工程師 Leo de Moura 花了十年打造一套叫 Lean 的程式語言，本來是幫軟體工程師抓 bug 的。結果軟體工程師沒怎麼理會，反倒是一群數學家把它當成了聖杯。書的副標題叫「一部真理機器如何改變數學與 AI」。真理機器這個詞很精準：你把一段數學證明翻譯成 Lean 能讀懂的語言，它會像一個極端嚴格的審稿人，逐行檢查每一步推論。全部通過，你就得到了一件傳統數學界無法提供的東西，百分之百的確定性。

讓這本書從技術史躍升為一個好看的故事的，是書中的人物。特別是最後壓軸登場的那位：菲爾茲獎得主、被視為當世最強數學家的陶哲軒（Terry Tao）。這位兩歲就教六歲小孩數數、十歲就拿國際數學奧林匹亞銅牌的天才，做了一件讓數學界跌破眼鏡的事。他開始學寫程式，而且用的就是 Lean。

數學家的信任危機：為什麼需要真理機器

要理解陶哲軒為什麼做出這個選擇，得先回到一個讓整個數學界尷尬了十幾年的故事。

1998 年，密西根大學數學家 Tom Hales 完成了一項歷史性壯舉：他證明了克卜勒猜想（Kepler conjecture）。這個猜想源自 1611 年，天文學家克卜勒在布拉格的查理大橋上看著雪花飄落，想到了一個問題：球體怎麼堆疊最有效率？答案直覺上很明顯，就是水果攤堆橘子的方式，金字塔形排列，能填滿大約 74% 的空間。但三百多年來，沒有人能嚴格證明這就是最佳解。Hales 花了五年，結合三百頁的理論論證和三 GB 的電腦計算，終於做到了。他把證明投到數學界最頂級的期刊《Annals of Mathematics》。

然後等待開始了。通常期刊會找兩三個審稿人，但《Annals》一口氣指派了十二個。一年過去，編輯說需要更多時間。兩年過去，同樣的回覆。三年、四年，依然沒有結論。審稿人看過的每一個部分似乎都是對的，但證明整體是一座龐大的計算迷宮，埋在電腦程式碼深處，沒有人能確定所有部分是否真的拼在一起。2002 年六月，其中一位審稿人寫信給編輯，說他不想開始檢查自己負責的部分，除非先確認其他部分是對的。換句話說：萬一整個證明最後是錯的，何必浪費力氣？

到了 2003 年一月，Hales 在巴爾的摩的聯合數學會議上發表演講。他先引用了《Annals》編輯的來信：「審稿人無法確認證明的正確性，而且未來也不可能做到，因為他們已經用盡了能投入這個問題的精力。」也就是說，數學界最頂級的期刊告訴他：我們做不到。Hales 在台上宣布，他要把整個證明重寫成一種電腦可以檢驗的形式語言。他估計這需要二十個「工作年」。他把這個計畫命名為 Flyspeck。

這個計畫最終花了十二年才完成。但它證明了一件事：電腦確實可以百分之百驗證一個人類無法完全檢查的證明。

Scholze 的求助信：當最強數學家也不確定自己對不對

如果只有 Hales 這樣的「非典型」證明需要機器驗證，Lean 可能永遠只是數學界的邊緣工具。真正讓局面改變的，是一封 2020 年 11 月的電子郵件。

寫信的人是 Peter Scholze。這個名字在數學界的份量，大概等同於物理學界的愛因斯坦等級。他 2018 年拿下菲爾茲獎，但那不過是確認了數學界早已知道的事：這是半個世紀以來最有天賦的數學家。Scholze 以快速消化其他人複雜證明的能力聞名，他的判斷幾乎等同於最終裁決。2018 年，當日本數學家望月新一發表了一份五百頁的 abc 猜想證明，數學界爭論多年無法定論時，Scholze 和同事花了一週審查，然後發表了一篇直白的論文：〈為什麼 abc 仍然是一個猜想〉。從此再沒有人認真討論望月的證明了。

但 Scholze 寫給倫敦帝國學院數學家 Kevin Buzzard 的那封信，卻是在求助。他和合作者 Dustin Clausen 發展了一套叫做「凝聚數學」（condensed mathematics）的新理論，要為拓撲學這個核心數學領域重建基礎。其中一個關鍵定理，Scholze 認為是他職業生涯最重要的成果，但他自己不確定證明是否正確。

不確定的原因很人性。這個證明極其複雜，Scholze 花了整個 2019 年夏天在腦中組裝這個論證。它的邏輯嵌套深度達到六層量詞交替，任何兩個量詞都不能交換順序。有一天下午他覺得離完成只差最後一步，於是晚上跟同事去酒吧慶祝，喝到很晚。隔天宿醉未退，他知道如果不趁現在把最後一步想通，整個證明可能又會從腦海裡消失。於是他頂著頭痛硬撐，到了傍晚終於想通了。「那個關鍵常數與 Lambda 無關，所以證明成立。」

但之後寫成論文的過程中，他開始懷疑自己。他想起年輕時在德國數學奧林匹亞國家隊的經歷：他曾經提交兩個自認完美的解答，拿了滿分，但後來自己發現兩個都是錯的。他也曾以為自己解決了一個重要猜想，專家也確認了，但幾天後他自己找到了致命的錯誤。Scholze 比任何人都清楚，他的說服力有時候太強了，強到連專家都可能被他帶著走而忽略錯誤。

所以他問 Buzzard：有沒有可能用 Lean 來檢查這個證明？

Buzzard 當然說好。他找來了 Lean 社群中最熟悉 Scholze 工作的 Johan Commelin 來主導這個計畫。Commelin 一開始很猶豫，他擔心自己會花好幾年鑽進「Lean 洞穴」，出來之後告訴數學界「好消息！Peter 的證明是對的！」然後大家回他一句：「廢話，Peter Scholze 做的當然是對的。」為了讓這件事有意義，Commelin 請 Scholze 公開聲明這個形式化工作對數學是重要的，把他的名聲借給 Lean 這個計畫。

Scholze 在 2020 年 12 月 5 日發表了一篇部落格文章，公開向 Lean 社群提出挑戰。他稱之為「liquid tensor experiment」（液態張量實驗）。到了 2021 年 5 月，Commelin 就完成了最核心的第一階段驗證。Scholze 在自己的部落格上寫道：「我太驚訝了⋯⋯我幾乎不敢相信形式化數學已經到了這個程度。」

陶哲軒的三幕轉變

Scholze 的液態張量實驗讓全世界的數學家注意到 Lean 已經不是玩具了。但要讓它從「有趣的實驗」變成「數學的未來」，還需要一個更具象徵意義的人物站出來。那個人就是陶哲軒。

書中詳細記錄了陶哲軒的轉變，大致分為三個階段。

第一幕是預言家。2014 年 11 月，陶哲軒和其他四位數學家一起出席突破獎（Breakthrough Prize）頒獎典禮的座談。當其他人在討論「數學是被發現還是被發明的」這類形而上的問題時，陶哲軒說了兩個讓全場覺得荒謬的預測：未來數學家可能會和幾百人同時合作一個問題；合作完成後，結果不是由人類審稿人檢查，而是由電腦驗證。他甚至具體描述了這會怎麼運作：「有一天我們可能不再用 LaTeX 寫論文，而是用某種語言寫，某個聰明的軟體會把它轉換成形式語言。偶爾你會收到一個編譯錯誤，電腦不懂你怎麼推導出這一步。」主持人和其他得獎者的反應是：這比我們活在數位模擬裡的假說還離譜。

第二幕是實驗者。陶哲軒其實很早就在嘗試大規模數學協作。2009 年，他和另一位菲爾茲獎得主 Timothy Gowers 一起發起了 Polymath 計畫，讓數十位數學家透過部落格留言區合作解題。計畫確實成功了，幾個月內就證明了一個定理，發表了數學史上第一篇以集體筆名「D.H.J. Polymath」署名的論文。2011 年，《華爾街日報》報導了這個計畫，稱它「開創了解題的新方法」。但陶哲軒很快意識到瓶頸所在。大規模協作增加了發現的機會，但也增加了犯錯的機率。唯一的防錯方法是找一個人仔細檢查所有人的工作，而這個瓶頸完全違背了 Polymath 的精神。他需要某種自動驗證機制。但在 2010 年代的技術條件下，這跟許願搭客機去火星差不多。

第三幕是行動者。2023 年 10 月 9 日，陶哲軒在社群平台 Mastodon 上發了一則帖文：「我決定終於來學 Lean 4 互動式證明系統。」他從 Kevin Buzzard 設計的「自然數遊戲」（Natural Number Game）開始，這是一個教人用 Lean 證明自然數基本性質的互動式教學關卡。陶哲軒中午開始玩，本來打算「有空再繼續」，結果一路玩到半夜就全部破關了。他發現這個遊戲會上癮，跟他平常刻意不跟小孩玩《文明帝國》是同一個道理：他知道自己一旦開始就停不下來。

學會基本操作後，陶哲軒立刻找了一個真正的數學問題來試手。他在 MathOverflow 上看到一個關於 Maclaurin 不等式的提問，先用傳統方式寫了十頁的證明，然後試著把它翻譯成 Lean。他很快發現一個意想不到的現象：證明中困難的部分在 Lean 裡反而容易，簡單的部分卻極其麻煩。就像 Buzzard 之前的經驗一樣，你在紙上寫「顯然三個大於一的數相加至少等於三」不需要任何解釋，但 Lean 不接受「顯然」。你得翻遍 Mathlib 函式庫找到一條引理來支撐這個「常識」。

PFR 猜想：三週形式化的壯舉

陶哲軒真正讓數學界震動的，是接下來發生的事。

2023 年 11 月 9 日，也就是他把第一個 Lean 證明上傳到 GitHub 三天之後，陶哲軒和三位合作者 Ben Green、Timothy Gowers、Freddie Manners 把一個重要定理的證明上傳到了預印本伺服器 arXiv。這是 PFR 猜想（Polynomial Freiman-Ruzsa conjecture）的完整證明，一個源自 1960 年代、關於集合的「和集」結構的重要問題。簡單說，如果一個數字集合的和集（把所有數字兩兩相加得到的新集合）出奇地小，那這個集合一定帶有某種規律，比如等差數列。

陶哲軒向三位合作者提議用 Lean 形式化這篇論文。Green、Gowers 和 Manners 對學 Lean 興趣不大，所以陶哲軒自己上了。但他知道以他的名氣，不會孤單太久。

11 月 13 日，他在 Lean 社群的 Zulip 聊天室開了一個新頻道，宣布要形式化 PFR 猜想的證明，歡迎志願者加入。一天之內，斯德哥爾摩大學博士生 Yaël Dillies 就用工具建好了專案的藍圖，把證明分成十三個章節。陶哲軒在每個章節裡把證明拆成五行一個的小引理，讓盡可能多的人能做出小貢獻。

這是 Polymath 2.0 版本，但這次有了 Lean 作為品質保證。任何人提交的程式碼，Lean 會自動驗證是否正確，不再需要一個人工瓶頸去檢查所有人的工作。志願者湧入了：「我想認領均勻隨機變數的熵 :)」、「我來試試一般纖維恆等式」。到了 11 月底，陶哲軒自己已經很少寫 Lean 了，他變成了一個忙碌的志工協調人，不停為別人找任務。有人完成任務的速度令人咋舌：他在 Zulip 上發布一個小任務，四十六分鐘後就有人回覆了完成的 pull request。

12 月 5 日，整個形式化只剩最後一個 sorry（Lean 中的佔位符號，表示尚未完成的部分）。那個問題看起來極其瑣碎：證明集合 {0}、{1}、{2, 3} 是「兩兩不相交」的，也就是沒有元素同時出現在兩個集合裡。人類一眼就看得出來，但 Lean 要求嚴格證明。陶哲軒寫了大約一百行冗長的程式碼，逐一檢查每個組合。他在 Zulip 上抱怨：「一定有更好的方法吧。」Commelin 回覆說確實有，用一個內建的策略指令 decide 就能解決。幾個按鍵搞定。

從啟動到完成，PFR 猜想的形式化只花了三週。這件事的意義不只是速度快。陶哲軒在事後反思時寫道，他自己其實沒寫多少程式碼。「這對我來說是很鼓舞的，因為它暗示未來數學家可以領導 Lean 形式化專案，而不需要精通 Lean 程式設計。」

2200 萬個問題與實驗數學的誕生

PFR 只是前菜。2024 年，陶哲軒啟動了一個規模更大的計畫，叫做 Equational Theories。

起因是 2023 年七月，一個使用者在 MathOverflow 上問了一個看似簡單的問題：加法滿足交換律（x + y = y + x）和結合律（(x + y) + z = x + (y + z)），但交換律不蘊含結合律。那麼在各種代數運算定律之間，完整的蘊含關係長什麼樣？陶哲軒開始畫草圖，發現這幅地圖可能極其複雜。他曾半開玩笑地說這可能是個適合給大學生或 AI 工具做的計畫，暗暗希望有人接手。沒有人站出來。

到了 2024 年九月，陶哲軒決定自己來。他計算出，如果只看運算符號恰好出現四次的代數定律，大約有 4,694 條。每一條都可能蘊含或不蘊含其他任何一條，總共產生 2200 萬個邏輯推斷需要檢驗。他在部落格上宣布了 Equational Theories 計畫，並寫道：「像 Lean 這樣的證明助手語言，提供了一個克服這些障礙的潛在方法。」

計畫的架構體現了陶哲軒構想的「工具階層」。最底層是簡單的 Python 腳本，用來暴力測試最基本的情況。幾天之內，這些腳本就解決了超過 99% 的 2200 萬個問題。往上一層是自動定理證明器 Z3，它擅長搜尋反例來確認兩條定律之間是否存在蘊含關係。最頂層才是人類的巧思，處理自動工具解決不了的刁鑽案例。而整個過程的品質保證，全部由 Lean 負責。

陶哲軒像科學家觀察自己的實驗一樣，在 GitHub 日誌上記錄觀察。專案啟動第二天，他寫道：「這個專案的推進速度遠遠超出我的預期。我以為三週完成的 PFR 專案已經夠快了，但這個又快了一個數量級。」一個月之內，2200 萬個問題被縮減到 238 個。到了年底，剩 30 個。到 2025 年三月，卡在最後 4 個上。貢獻者們一個一個嘗試，很多人慢慢散去。

但完全解決 2200 萬個問題從來不是真正的目標。陶哲軒把 Equational Theories 視為一種全新數學方式的先導實驗。在他看來，這是「實驗數學」的開場：就像物理學從理論為主的學科演變出實驗分支一樣，數學也可以有大規模協作、工具驅動、機器驗證的實驗模式。一個人或一小群人絞盡腦汁攻克一個問題的時代不會消失，但旁邊會出現另一種全新的研究方式。

真理機器的下一步

《The Proof in the Code》出版的時間點很微妙。2024 年，Google DeepMind 的 AI 系統在國際數學奧林匹亞上拿到了接近金牌的成績，核心元件 AlphaProof 用的正是強化學習搭配 Lean 的方法。AI 實驗室紛紛投入資源，希望打造「AI 超級數學家」，不是為了解數學題，而是因為他們相信數學推理能力是通往通用人工智慧的關鍵拼圖。在這些努力中，Lean 扮演了核心角色：它能提供清晰的回饋訊號，驗證不可靠的大型語言模型的輸出。

Leo de Moura 在 2023 年離開微軟，加入亞馬遜雲端服務，同時擔任 Lean 專責研究組織（Lean FRO）的無薪志工執行長。這個組織由 Google 前執行長 Eric Schmidt 創辦的 Convergent Research 支持，目標是讓 Lean 變得更容易使用，最終實現自我維持。Carnegie Mellon 大學的 Jeremy Avigad 則在打造 Lean 版的 Sledgehammer，一個能用神經網路從 Mathlib 的數十萬條定理中挑選相關素材，然後自動建構證明的工具。

但最能說明 Lean 已經跨過臨界點的，可能還是陶哲軒的態度轉變。這位曾經被認為最適合單打獨鬥的天才數學家，現在是 AI 輔助數學的頭號佈道者。他在 2024 年的兩場重要演講中描繪了一個願景：人類的洞察力、大型語言模型的創意、以及形式化驗證系統的正確性保證，三者結合形成一種新型態的數學協作。他承認目前的 AI 工具在數學前沿表現不佳，像是「過度自信的大學生」，會提出建議但分不清好壞。但他看到了一條路：把複雜問題拆成數千個小問題，讓 AI 處理最簡單的那些，人類專注於最困難的，而 Lean 負責確保所有結果都是正確的。

十二年前，Hales 宣布要花二十年把一個證明翻譯成機器可讀的形式語言，當時在場的數學家大概覺得這是走投無路的瘋狂之舉。今天，陶哲軒三週就能帶領幾十個人形式化一個重要定理，然後轉身啟動一個 2200 萬個問題的計畫，讓機器和人類分工合作，不到一年就幾乎全部解決。真理機器不再是邊緣工具，它正在重新定義什麼叫做「做數學」。