一小群人如何打造「真理機器」，以及為什麼前沿 AI 隨手可用的時代，會讓 Lean 更重要？
這篇文章以《The Proof in the Code》的 Part I–III 為主，後半加入 2026 年 7 月 15 日以前的 AI 數學進展。本書的主要敘事大致停在 2025 年初，Erdős #1196、單位距離（Unit-Distance）反例、KTV 和 Cycle Double Cover Conjecture 都是本書出版後才出現的新故事，這篇文章的大部分數學證明過程都是由 GPT-5.6 Sol Ultra 協助完成，由我進行修訂。
我大概還需要幾天才會寫我這半年如何使用 ChatGPT-Pro 以及 Codex 做科學研究，不過由於更大量地使用這些工具，以及我的好朋友、我所認識的最聰明之人「貍貓」常常分享的形式化驗證，讓我想深入了解 Lean 這套工具。而就這麼剛好，今年出版了《The Proof in the Code》，而且這個出版時間我認為比過往任何時候都要重要，原因在文章後段會解釋。這本書的作者是 Kevin Hartnett，他是 Quanta Magazine 的資深作者（Quanta Magazine 可以理解成更硬核、深入的科普網站），負責電腦科學和數學的主題，由他來撰寫 Lean 的發展史可說是相當適合。
我跟貍貓都很驚訝竟然會有人想寫這樣的小眾數學工具，不過隨著如今 GPT-5.X 系列和 Claude 家族的 Fable 系列展現出遠超人類數學家的推理能力，一個從未受過專業數學訓練的人，也能調用大模型來解決數學問題，但是誰來驗證這些證明？是否具備這樣的「真理機器」來進行驗證？這個工具的新生和崛起就是本書想述說的。如果你只想知道 GPT-Pro 最近又解掉哪些數學題目，FrontierMath 排行榜和數學家推文就很夠了，《The Proof in the Code》將鏡頭拉回 AI 遠未成為顯學的年代，看看一小群數學家、電腦科學家、教師和維護者，如何花上數十載，把一件當時沒有多少人相信有用的事情，慢慢做成當代最有偉大的數學家陶哲軒親自使用、Google DeepMind 和 OpenAI 也在代表性研究中採用的重要基礎設施。
“Everything is vague to a degree you do not realize till you have tried to make it precise.”― Bertrand Russell
我在五月曾寫過一篇很短的 《Lean into the Future》，這篇備忘錄般的短文的標題也是取自本書其中一章，當時想記下的感覺是：前沿模型的能力已經強到有些荒謬，同一個東西可以替你整理信件，也可能證明一個困擾數學家多年的問題，現在的瓶頸逐漸變成人類能不能提出夠好的問題、設計夠好的流程，並且讓模型能發揮其完整能力。
在我上個月飛到福島機場、準備南下去東京看 =LOVE 的盛大演出時，我在去程的飛機上看完了這本《The Proof in the Code》（我紙本書跟電子書都有買），非常有啟發、也非常激勵人心，儘管數學、理論電腦科學、程式碼、或 10 年前被 AlphaGo 征服的圍棋領域，這些學問有一個共同特性，就是答案是非分明，這種特性的學科，能夠設計出驗證器（verifier)，甚至是基於自然語言而非形式語言的驗證器，而且這個驗證器與自然科學、工程學不同，不需要外部的 oracle，我不免會構想在更廣泛的科學領域，能否也使用這樣的 prover-verifier 架構？
一張掛在牆上的通緝令
《The Proof in the Code》從一件近乎荒謬的事情開始：Tom Hales 證明了克卜勒猜想，數學共同體卻沒有足夠能力確認他真的證明了它。
Hales 和 Sam Ferguson 的證明包含約三百頁論證與大量電腦計算，《Annals of Mathematics》動用十二位審稿人，耗費多年，最後仍只能確認各部分看起來大致合理，無法用傳統方式替整體背書。Hales 把最後五十種棘手的球體配置做成「通緝海報」，貼在辦公室牆上，每排除一種就撕下一張；最後一張海報消失時，數學問題似乎已經結束，信任問題才剛開始。
如果連十二位專業審稿人耗費多年都無法完整驗證一份證明，「證明」這兩個字究竟還意味著什麼？
Hales 後來發起 Flyspeck，用 Isabelle 和 HOL Light 將證明完整形式化。請注意，Hales 不是 Lean 使用者，克卜勒猜想也不是由 Lean 驗證；他在這本書中的位置，更像是替 Lean 類系統提出了無法迴避的需求。Computer-assisted proof 可以依靠自訂程式、龐大計算和輸出，formal proof 則要求每一步推導最終都能被一個小型 checker 依照明確規則重演。在形式推導這一層，人們不必只依賴幾百頁程式碼和審稿人的直覺，大部分信任被壓縮到形式命題、選定公理、kernel 與其 trusted computing base；問題沒有消失，只是範圍縮小了，也更容易公開檢查。
Part I 的標題是「Visionaries」，讀起來卻更像一段漫長的工程史。Lean 沒有某位天才忽然想通一切的時刻，而是一群人從不同問題出發，最後慢慢在某個路口會合，然後朝同個方向邁進。Leo de Moura 從 Yices、Z3 與軟體驗證一路走來，很清楚 SAT／SMT 系統有多強，也知道完全自動搜尋一旦遇到需要發明中間概念、行動空間又近乎無限的研究數學，很容易失去穩定性。Jeremy Avigad 則站在另一側，他理解數學家如何依靠抽象、慣例與大量「顯然」工作，也知道 proof assistant 不接受這種默契。
Lean 最後採取 interactive theorem proving：人類決定命題、定義、方向與中間概念，機器負責檢查每一個推導是否合法。Curry–Howard correspondence 讓命題可以被看作型別、證明可以被看作程式；kernel 不需要欣賞證明是否優雅，它只需要足夠固執，任何沒有根據的跳步都不准通過。
書裡每個人擔心的事情都不太一樣。Hales 想確認超大型證明是否可信，de Moura 面對完全自動搜尋的邊界，Avigad 和 Georges Gonthier 則得處理數學家與機器使用兩種語言的麻煩；他們也會爭辯、走錯路、重新來過。Lean 就像這群執著的數學家多年協調後留下的共同作品，而不是一開始便設計完整的「真理機器」。
真理機器也需要人類維護
進入 Part II「Early Adopters」後，書裡開始出現許多不太為人所知，但 Lean 少了它們卻一步也走不動的工作項目。一個 kernel 可以完全正確，外面仍是一片荒地；早期 Lean 幾乎不懂數學，整數、實數、群、環、拓撲空間和數不清的基礎 lemma，都得有人一個個補起來。
Mathlib 就是在這片荒地上長出來的。Avigad、Rob Lewis、Floris van Doorn、Mario Carneiro 等人做的工作，更接近重新編排數學：哪些定義先出現、抽象應放在哪一層、下游定理依賴什麼介面，全都得重新決定。原本散落在論文、教科書與專家腦中的知識，逐漸成為可以搜尋、重用、組合，並建構會留下版本歷史的公共程式庫。
Kevin Buzzard 是這部分相當有意思的一號人物，他對 p-adic Langlands 周邊論文層層相疊的信任鏈感到不安，擔心一篇論文依靠另一篇論文、最後又依靠少數權威人物的默認。這當然不能直接推論成整個領域都不可靠，卻足以解釋他為何對 Lean 產生近乎傳教式的熱忱。他一開始想用 Lean 教大學生，結果發現 Mathlib 連複數都還沒有，簡單問題也得先補建大片基礎（教學實驗沒有照預期成功，反而把還缺乏什麼暴露得更清晰）。
後來 Buzzard、Johan Commelin 和 Patrick Massot 決定形式化 perfectoid spaces，還坦白承認這是一場吸引主流數學家注意的 stunt。這個策略很有效：如果 Lean 連即將獲得 Fields Medal 的 Peter Scholze 所發展的核心物件都能表達，就很難再說形式化只能處理小學算術。更重要的是，為了抵達 perfectoid spaces，他們沿路建立 valuation、adic space、uniform space、topological algebra 和 sheaf 等大片基礎，最後留下超過三千個節點、三萬條邊的依賴圖。
形式化最有價值的產物，往往不是終點那一個 theorem，而是沿途蓋好的道路。數學定理不會因軟體升級而變假，承載它的 proof code 卻會壞；有人得修復證明、審查 pull request、協調互相衝突的定義、回答新手問題，還要確保 Mathlib 擴張後依然有人敢碰。小型 kernel 守住邏輯底線，Lean 能不能成為大家都能使用的工具，則要看維護者、教師、文件、Zulip、版本治理與長期經費能不能跟上。
形式化沒有拿掉人類的角色，只是把原本藏在權威、默契和「讀者自行補齊」裡的工作攤到陽光下，如子標題所說：真理機器依然需要人類的維護。
當裁判開始訓練選手
Part III「Influencers」把 Lean 帶進前沿數學和 AI。Scholze 與 Dustin Clausen 的 liquid tensor experiment 是一場精彩的壓力測試：紙面上六頁密集估計可以相對快速地形式化，五行「由此可得」反而需要補建 Abelian categories、cohomology、Ext groups 和 derived functors 等大片背景。論文寫得短，不代表證明成本低；很多時候只是共同體替作者保存了大量不必明說的知識。
團隊把尚未完成的 lemma 用 sorry 標記，公開成任何人都可以認領的工作，二十八位貢獻者各自完成局部內容，最後再由 Lean 檢查能否安全拼接。這裡的 Lean 已經不只是 verifier，也是一種低信任的大型協作協定：你不必熟悉每一位陌生貢獻者，只要他提交的 proof object 能通過檢查。
Google DeepMind 的 AlphaProof 則把 Lean 用到了另一個方向。模型每產生一步 Lean code，Lean 都會回傳 proof state；它在終點檢查答案，也在過程中告訴模型這一步能不能走。Mathlib 同時是知識庫、工具箱和可重用的訓練環境。AlphaProof 加上 AlphaGeometry 在 2024 IMO 得到 28 分、銀牌水準，距離金牌只差一分。
不過這並不是和人類完全公平的競賽：題目由團隊人工形式化，有些題目提供多個版本，AlphaProof 每題可以運行到三天，幾何題又交給專用系統處理；正因為題目還需要人工形式化，使得模型縱使可處理高度符號化的證明，卻也可能先在「題目到底說了什麼」這一關跌倒。
陶哲軒的出場，讓這段技術史變成了真正的、數學工作方式的實驗史。他早在 2014 年便想像未來會有數百人合作的數學項目，論文會像程式一樣顯示 compilation error；Polymath 讓他體會大型協作的創造力，也讓他看見人工主持與驗證會成為 bottleneck。Liquid Tensor Experiment 改變他對 proof assistant 實用性的評估，後來他學習 Lean、參與 PFR formalization，再把 Python、Z3、自動定理證明器、AI、人類反例與 Lean 接進 Equational Theories Project。
陶哲軒在數學方面的驚人成就，我相信維基百科的條目寫得比本文清楚，他對自動化定理證明的熱忱倒是被低估了。陶哲軒關心的是怎麼重新分解數學工作：有人選問題，有人建立定義與介面，有模型進行大規模搜尋，有 Lean 檢查 proof object，最後仍要有人把結果放回文獻、提煉成可以理解和傳授的概念。2026 年他把這套流程分成 proof generation、proof verification 和 proof digestion；前兩步正快速被 AI 與形式系統加速，第三步仍是人類專家必須承擔的責任。
讀到陶哲軒這一段，一切似乎都銜接起來了，包括早期那些看似瑣碎的工作。早年 Lean 還得靠 perfectoid stunt 爭取主流數學家的注意，後來陶哲軒用它組織大型協作，DeepMind 把它放進 AlphaProof 的核心，OpenAI 也早在 2022 年公開以 Lean 研究 neural theorem proving。這個小圈子的理想終究破繭而出；一代代使用者將其傳承、改良下去，最後構建出下一個時代需要的公共工程。
最後還得說說我們的老熟人、即使你看完這篇文章還是不知道這些數學家和電腦科學家是誰，你肯定聽過 OpenAI 的 CEO-Sam Altman。2021 年 de Moura 和 Daniel Selsam 就曾與之碰面，Sam 表示自己喜歡 Lean，也有雄心能訓練出一個解決千禧年問題的 AI 模型，雖然他不打算聘用任何人在 OpenAI 內專門做 Lean 相關的開發工作，但他很樂意捐款給支持 Lean 開發的非營利組織。雖然 de Moura 對 Sam 的提議不感興趣，不過 Daniel Selsam 倒是被其打動而加入 OpenAI，就我目前能查到的公開資料，他時至今日依然仍在 OpenAI 內。當你接著觀察這半年來，GPT 模型家族幾乎制霸了大多數 AI 數學證明、不少數學家或業餘數學家，透過 GPT 模型能解決 Erdős 猜想，你就會發現：Sam Altman 的雄心以及對數學的支持，可能是認真的，而且我的確認為他們有可能解決其中幾個「比較容易」的千禧年猜想，例如
最可能透過 AI 搜尋候選奇異解、再由 computer-assisted proof 完成的 Navier–Stokes existence and smoothness，又或者是最符合 AI 在代數、數論、定理檢索與形式化方面的現有強項的 Birch–Swinnerton-Dyer conjecture 。
補充：OpenAI 在 2026 年 9 月 8 日宣稱解決了 Navier–Stokes 問題，使用的是比當前 SOTA 模型-GPT-6-Astra 更強的內部模型，符合我的預測，但也比我預期的更快，非常可怕的進展速度，也許下一個會是 Birch–Swinnerton-Dyer conjecture？過程中跟 Anthropic 方也有一些學術上的恩怨、各說各話，不過縱觀數學史，例如萊布尼茲和牛頓的微積分之爭，這根本是司空見慣，讓我們一眾渺小人類繼續感受 SOTA 模型在數學上的雄偉進展吧。
未來已至，奇點鄰近
《The Proof in the Code》在 2026 年才出版，後半部卻已經需要補寫續篇。它的主要敘事大致停在 2025 年初；此後從 GPT-5.2、GPT-5.4、GPT-5.5 到 GPT-5.6 Sol 等 Pro 版本、Codex 下運作的工作流、甚至只是 thinking mode，AI 在研究數學上的進展，已快到書本剛落地就開始追不上。
很顯然我並非 primitive sets、代數數論或圖論這幾個子領域的研究者，也無法替 Erdős #1196、單位距離反例或 Cycle Double Cover 的證明裁定最終歷史地位，不過還是值得書寫這些前沿 AI 在數學的進展：模型是否提出關鍵想法、Lean 究竟驗了什麼、專家是否找到先驅脈絡，以及共同體是否已把結果消化成可以傳授的數學。令人驚嘆的是，即使把標準拉到這麼嚴格，最近幾個月的進展仍然一次次讓數學界震撼，如果你足夠關注的話。
在此之前已經有不少 Erdős 猜想被 GPT-Pro 攻破，只是有些更像是不被主流關注的長尾問題，而 Erdős #1196 可能改變了一切。這個問題研究一類稱為 primitive set 的正整數集合。先挑一個很大的門檻 x，集合裡所有數都不得小於 x，而且任何兩個不同元素都不能整除彼此。接著替集合中的每個數 a 指派一個權重：用 1 除以「a 與 a 的自然對數之乘積」，最後將所有權重加起來。Erdős 問的是，當門檻 x 越來越大時，這個總和是否必然不超過 1 加上一個逐漸消失的誤差；直觀地說，不論怎麼挑選 primitive set，它的漸近總重量能不能由常數 1 壓住。
Liam Price 把問題和當時的最佳一般結果交給 GPT-5.4 Pro，沒有提示 Markov chain 或 von Mangoldt 方法。舊結果只能保證這個總重量漸近不超過約 1.399，再加上一個會消失的誤差；模型在約八十分鐘的長推理後，將前面的常數降到猜想要求的 1，還給出更明確的收斂速度：剩下的誤差可以由某個固定常數乘上「x 的自然對數之倒數」控制，所以 x 越大，容許的誤差上界便越接近零。
它的做法是先按照「誰能整除誰」排列正整數，便會得到一個 divisibility poset；primitive set 中沒有兩個元素可以互相比較，所以恰好形成 antichain。接著，模型在這個偏序上設計一條隨機向下移動的 Markov chain：走到整數 n 時，選擇一個整除 n 的質數冪 q，再從 n 走到 n 除以 q。每個 q 被選中的機率，是用它的 von Mangoldt weight 除以 n 的自然對數；所有候選 q 的 von Mangoldt weights 加起來又剛好等於 n 的自然對數，因此這些數值確實構成一組總和為 1 的轉移機率。
到這裡還沒有證完。論證還得證明原問題使用的「1 除以 a 與其自然對數之乘積」這套權重，在向下移動後不會憑空增加；技術上稱為 sub-invariant weight。再利用這個性質把過程反轉，便能構造一條 adjoint upward chain，並替它安排適當的初始 mass：每個整數 a 所接收到的命中 mass，足以控制原問題賦予 a 的權重，而所有初始 mass 的總量，又不超過 1 加上一個可由「x 的自然對數之倒數」控制的誤差。任何一條整除 chain 最多只能碰到 antichain 一次，因此整個 primitive set 接收到的命中 mass 不可能超過初始 mass；這才把機率敘述真正翻譯成需要的解析上界。後來的預印本又把這個想法發展成可推進其他問題的 chains／flows 框架，陶哲軒的研究紀錄則指出，相關文獻搜尋沒有找到這個關鍵接合方式。
Markov chain、von Mangoldt function 和 primitive sets 都不是模型發明的，這個問題也有八十多年研究脈絡；新意在於模型認出這些材料可以用一種此前未見於相關文獻的方式接在一起，而且這個 proof architecture 還能繼續產生定理。若把 AlphaTensor、FunSearch 等專用系統也算入 AI 數學史，#1196 當然不能毫無限定地寫成「史上第一次 AI 原創數學」；但若討論通用對話式 LLM 在自動數學中解題銜接兩個人類意想不到的領域、搭建可信服的方法橋梁，它是目前證據鏈最完整、也最令人信服的早期案例之一。
典範需要新的基本對象、一整組能繼續延伸的問題，以及共同體可以共享的解釋語言；#1196 的文獻定位、一般化、命名與數學價值，主要仍由 Price、陶哲軒和其他作者完成。但這個案例至少改變了許多人的認知和判斷：LLM 已經不只會執行人類指定的方法，它有時能重新表示問題，並找到原先分開的工具之間可以接上的位置。這離典範轉移還很有段距離，卻也不再只是高效率的 cleaning task，而是 LLM 真能超越人類既有的認知邊疆。
單位距離反例把同一件事推到更大尺度。這個問題問的是：在平面上放置 n 個點，最多能讓多少對點之間的距離剛好等於 1？Erdős 原先猜測，即使採用最巧妙的排列方式，答案也只能比 n 線性成長稍快一點；更精確地說，雖然指數可以略高於 1，但那個多出來的幅度應隨 n 增大而逐漸消失。
2026 年 5 月，一個未命名的 OpenAI 內部通用推理模型（目前看來很可能是 GPT-5.6），把 growing-degree CM fields、class-field towers、bounded root discriminant 和幾何格點構造接在一起，推翻了這項猜測。模型證明存在一個單一、固定的正數 delta，並且有一串可以任意變大的 n；對這串 n 中的每一個值，都能找到一組平面點，使單位距離的點對數至少達到「n 的一加 delta 次方」。換個方式說，這不是只比 n 多上一點對數修正，而是 n 還要再乘上一個固定正次方的多項式因子（這項結果沒有宣稱所有充分大的 n 都達到同一個下界，也沒有求出最大單位距離數的真正漸近）。
Boris Alexeev 以 human-in-the-loop Codex 工作流和 GPT-5.6 產生約一百二十萬行 Lean 來進行形式化驗證（也就是本文介紹的工具），目標定理及其可達依賴閉包通過 lean-eval 的 comparator 和 Lean kernel。這代表該目標及其可達依賴閉包不含 sorry 或未准許公理，不代表整個 repository 已經逐行接受人類審稿。推文所說的 exponential rate 也很容易被誤讀：證明中的某些中間量，會隨輔助數域的 degree 呈指數成長；但把它換算回平面點數 n 後，最後得到的仍是多項式，只是多項式的指數確定比 1 多出一個固定正數。它不是說單位距離數會像二的 n 次方那樣爆炸。
Guanyang Wang 對 Kannan–Tetali–Vempala（KTV）猜想二元矩陣情形的案例又補上另一種人機閉環：GPT-5.5 Pro 經少量提示產生證明，人類將它從失敗路線導向代數方法並檢查數學，Codex 再花約一百小時，把自然語言論證轉成重構後七至八萬行 Lean。Timothy Gowers 的經驗沒有形式驗證，卻得到領域專家 Rajagopal 對原創性和正確性的高度肯定（當然，Timothy 本人是 Fields Medal 得主，他的洞見很可能不需要所謂的「專家」去認證）。兩個案例都沒有從零建立新理論，但「所有材料早已存在」不等於「沒有創造」；據作者和領域專家的查核，辨認出一個未見於相關文獻的全域結構，本身就是研究數學。
到了 7 月 10 日，OpenAI 公開一篇聲明由 GPT-5.6 Sol Ultra 產生的三頁證明，並表示該系統使用最多 64 個並行 agents；另有約七千行 Lean 形式化，主定理的 axiom audit 只使用 Lean 的標準公理。
這份 Cycle Double Cover 證明使用的是一條至少可以追溯到 1983 年的 8-flow／cycle-cover 路線。標準的 nowhere-zero 8-flow，是先替圖的邊指定方向，再讓每條邊攜帶一個絕對值小於 8、但不能等於 0 的整數流量，並要求每個頂點的流入與流出守恆。Tutte 的 group-flow theorem 告訴我們，8-flow 的存在性也可以等價地改寫成：在任意一個具有八個元素的交換群上，尋找 nowhere-zero flow。這篇證明選擇的群，可以想成所有三位元的 0／1 標籤；標籤相加時，每一位都只看奇偶，所以兩個 1 相加會回到 0。每條邊取得一個非全零的三位元標籤，而在化約後的三度圖中，每個頂點相接的三個標籤加起來都是全零。
舊理論早已知道這類 flow 與 cycle cover 有密切關係，困難在於怎麼讓各頂點分別作出的局部安排，在同一條邊的兩端得到完全相同的結果。新證明不是從兩個向量中挑選一個；它替每條邊保留整個二元素 affine pair：先取一個三位元向量，再將它和該邊原有的 flow 標籤相加，得到 pair 中的第二個向量。線性對偶論證證明，可以調整每個頂點的 offset，使一條邊從兩端計算出的 affine pair 在全圖上彼此一致。
最後，對八元素群中的每一個標籤，收集所有 affine pair 包含該標籤的邊，便得到八個子圖；在每個頂點，某個標籤只會完全不出現，或者剛好出現兩次，所以這些子圖都能拆成彼此不相交的 cycles。另一方面，每條原始邊的 affine pair 恰好含有兩個標籤，因此它會出現在八個子圖中的兩個，最後也就被 cycles 恰好覆蓋兩次。這正是 cycle double cover 所要求的結果。
因此，這項成果已不能被簡化成一則沒有證據的社群傳聞；同時，完整 agent trace 尚未公開，自然語言證明仍未完成傳統同儕審查，先驅脈絡也相當清楚。比較成熟的評價，是承認模型在既有 8-flow 路線上找到一個出人意料、可由形式系統重檢的 global-compatibility 轉折，而非立刻宣告它建立了全新典範。
低垂的果實會越來越成熟
寫到這裡，我想到睿智的朋友貍貓提出了「低垂的果實」觀點。所謂「低垂」，並不是說這些題目很簡單；那些 Erdős 猜想可能已經困擾人類數十年，問題本身不會因 GPT 問世就失去歷史價值。改變的是工具和瓶頸之間忽然出現新的契合：文獻爬梳、定義澄清、baseline 重建、反例搜尋、程式實作、局部推導、失敗路線排除和論文整理，可能在一次模型更新後變得便宜很多。昨天還掛在樹冠上的果實，今天已經伸手可及。
我在臨床 AI 研究中看過相同的成本位移。2023–2024 年，把 LLM 用於醫學報告理解、鑑別診斷或 board-style questions，可以建立當時尚不存在的能力 baseline；到了今天，如果只是更換疾病、影像模態、資料集或模型，再重複同一套 agreement protocol，科學增量往往只剩低成本的橫向複製。早幾年把另一種醫學影像丟進 U-Net，再報告一次 Dice 分數，也經歷過相同的邊際資訊遞減。
這些工作未必完全沒有價值。特定語言、罕見疾病或在地臨床流程仍可能需要自己的驗證，但臨床效用、方法新穎性與期刊可發表性本來就是三種不同的東西。當 benchmark 變便宜，真正昂貴的問題會移向跨院外部效度、calibration、前瞻性人機工作流、人與模型的錯誤會互相抵銷還是放大、臨床決策是否改變，以及病人結果是否改善。醫療沒有相當於 Lean kernel 的終局裁判，診斷更準也不保證病人活得更久或活得更好。
數學的 cleaning task 也值得更公平的評價。AI 如果能重建散落文獻、統一符號、測試被遺忘的構造、排除大量無效路線並補齊論證，它保存的不是比較整齊的文字，而是過去沒有被系統化的負面知識：哪些方法試過了、為何失敗、哪些假設不能拿掉。這些工作不一定創造新數學語言，卻能替下一次發現搭好梯子；#1196 的特別之處，就在於模型沿著這架梯子再往上一步，認出一座可以繼續拓展未知數學的工具橋梁。
低垂果實會移動，而且移動得越來越快。今天的難題會成為明天的整理題，今天的整理題又會成為後天的 baseline；誰能最快辨認新工具剛好解除了哪個舊瓶頸，誰就可能先採到這一輪成果。趁同質化尚未完成時快速發表，當然是合理的研究策略，我自己大概也會這麼做；但如果一輪工具紅利最後只多留下幾篇 paper，果實採完也就結束了。更值得做的，是把資料、形式函式庫、失敗路線與驗證管線留給下一個問題，讓短暫窗口變成後來的人仍能使用的研究基礎。
模型進步不會讓研究品味變得不重要，恰好相反。工具越強，越需要有人知道該往哪裡挖。
The age of Vibe-Mathing
Prompt era 或許很適合用來形容大型推理模型問世後的時代，每個「可能」存在答案的問題，都有機會使用一串 prompt 來解決。不是大家突然學會幾句神奇提示詞，然後就能瘋狂解決所有數學問題。比較接近的情況是：有人先選好問題與表述，將它拆給多個 agents，刻意保留互相競爭的路線，讓 critic 攻擊候選證明，必要時再呼叫程式和文獻工具，最後才把結果送進 Lean。
暫時把這種工作方式叫作 vibe-mathing（這其實來自前段提過的 Guanyang Wang 教授的取名），跟時下流行的 vibe-coding 有異曲同工之妙：用自然語言、工具呼叫、多代理協作和高速迭代，大量產生猜想、證明草圖、計算實驗與候選證明，再逐層收緊證據要求。
陶哲軒把這個變化稱為從 proof scarcity 走向 proof abundance。當候選證明的產生速度超過專家閱讀、形式化和查核文獻的速度，稀缺的便不再是多寫出一份證明，而是確認題目沒有被偷換、保存推導來源、讓其他團隊能夠重做、查明方法是否早已存在，最後再把結果消化成人能理解和傳授的數學。
如果技術正確、局部新穎但概念幅度有限的結果可以大量生成，中等成果的 publication premium 勢必會被壓低。它們仍可能有累積價值，可靠的負結果、lemma、資料集和驗證工具也不會突然失去用途；改變的是，「完成一項很多人都能迅速重做的工作」不再天然代表多年累積的稀缺勞動。
結論就是：vibe-mathing 越普及，Lean 越重要，這本數學工具史又更值得我們一讀。
候選證明越容易生成，數學共同體越需要低信任、可重現、可擴張的驗證層。Lean 可以檢查 proof object 是否在指定形式系統內成立，卻不能替我們判斷形式命題是否忠於原問題、證法是否早已存在、結果是否重要，也不能自動把一百二十萬行 proof code 壓縮成數學家願意閱讀和傳授的概念。生成、驗證和消化會逐漸成為三種不同的專業，數學家沒有離場，只是過去揉在一起的工作開始顯出各自輪廓。
OpenAI 長期投入 Lean-enabled theorem proving 與 AI 數學研究，從 2022 年的 neural theorem prover，到後來的 Ramsey proof、unit-distance 形式化和 CDC repository，都把 Lean 當成模型成果的可信度層。儘管本書記載的 2021 年捐助討論沒有讓 OpenAI 成為 Lean 核心的長期維護者，目前 Lean FRO 的公開 funder 名單也沒有 OpenAI，但他們深度支持以 Lean 為驗證工具的數學研究，我認為值得給 Sam Altman、Sébastien Bubeck 他們一份公允的評價，不論你怎麼看待 OpenAI 或這些領導層。
Lean together
縱觀全書，不僅是有趣的數學工具史，我自己更喜歡的是這種一群人橫跨多年、接力完成某項使命的熱忱與投入，也許在不遠的將來會出現一個大一統的超強智慧體，能夠獨力完成所有事情，但這種人類時代的浪漫我認為應該被保存下來。書中提到 de Moura 一直覺得人生最悲哀的事情就是沒有目的，他希望 Lean 是有用的、是可以達到預期的目的的，不論 Lean 未來會如何發展，也許被取代、被整合，或推出更完善的版本，這個小眾的工具已經達到它最初的目的了。
Lean 最初只是一小群人面對數學信任危機時做出的回答，Mathlib 維護者、教師與志願者把它擴建成公共工程，陶哲軒拿它組織大型協作，DeepMind 和 OpenAI 又把它帶進 AI 數學；走到今天，新的問題反而更多了：誰負責 statement alignment，誰承擔維護成本，這套公共知識又該向誰開放？以及我自己最想知道的：這種 prover-verifer 架構能否廣泛用於不同的科學領域？如何確保 AI 輸出結果是可證的？能因此加強人類在工作流中對 AI 產出之結果的信任嗎？
當最後一行程式顯示 no goals，kernel 能確認推導已經閉合，卻不知道這個 goal 值不值得設定。超人工智慧還有長遠的距離，而機器越能替我們驗證證明，或許人類更不應該盲目、大量地將問題丟給 AI，並拋下解釋結果和決定數學要往哪裡走的責任；現階段我們得更清楚地看見，哪些事情仍得由人負責，以及哪些題目是真正重要的，不論是數學、物理、統計、計算機理論皆然。
“Taste is all you need” 似乎是對的，或者至少在 AI 比人類更懂品味之前都是如此。
發表迴響