Claude 形式化費馬大定理：Lean 驗證了什麼、又沒驗證什麼？（2026）

2026 年 9 月 4 日，Anthropic 發布〈Formalizing Fermat’s Last Theorem〉，宣布由內部研究模型完成端到端 Lean 證明。Claude 形式化費馬大定理真正突破的不是發現一套新數學，而是把一條人類早已接受、卻橫跨大量現代數論的證明路徑，轉成可由機器逐步檢查的形式物件。

報告中的數字很容易讓人誤讀成「AI 用 11 天解開數學史難題」：約 1,300 萬行 Lean、約 3 萬個定理、60 億個輸出 Token，還有數十個代理協作。這篇文章會先還原它到底證明了什麼，再拆解 Prove2Me、Claude Code 多代理框架與 Lean 核心各自扮演的角色，最後回答一個更重要的問題：機器驗證完成之後，人類是否真的更理解這個證明？

先給結論：證明通過了，但三種主張要分開

• 有獨立成品檢查支持：公開 repository 的最終 Lean 命題就是一般形式的費馬大定理；數學家 Kevin Buzzard 表示，他已編譯程式並執行 Comparator，結果通過。
• 主要來自 Anthropic 自述：11 天、約 60 億輸出 Token、數十個代理與「大致相當於 Claude Fable 5.1」的內部模型，仍應按 Anthropic 這次 campaign 的自報數據解讀；Buzzard 的獨立檢查範圍是 codebase 與 Comparator。
• 不能由 Lean 通過推出：AI 發現了新證明、每個中間定理名稱都符合數學語意、成果容易閱讀與維護，或這套方法已具備可接受的成本效率。

因此，最合理的評價不是把成果降格成「只是把舊證明打字」，也不是把它升格成「AI 解決了費馬大定理」。它是一個規模極大的自動形式化與證明工程里程碑：新意主要在自動形式化與證明工程，而不是新的紙筆 FLT 證明。

Claude 形式化費馬大定理，實際完成了什麼？

費馬大定理說的是：當整數指數 n ≥ 3 時，不存在正整數 a、b、c 使 a^n + b^n = c^n。Andrew Wiles 在 1993 年宣布證明，之後與 Richard Taylor 修補缺口，論文於 1995 年出版。數學界早已接受結論；這次的新工作，是讓 Lean 4 的核心也能從明確定義與公理一路檢查到同一個終點。

公開的 FinalCheck.lean把終點寫成自然數版本：給定 n ≥ 3 與正整數 a、b、c，兩邊冪次之和不等於第三邊冪次。FinalCheck.lean 還由這個正整數版本推得 Mathlib 既有的 FermatLastTheorem；Comparator 分別把兩個公開目標與只依賴 Mathlib 的挑戰命題比對，避免只完成一個名字相似、內容卻較弱的替代品。

證明主幹不是逐頁翻譯 Wiles 論文，而是依循 Henri Darmon、Fred Diamond 與 Richard Taylor 對 Wiles／Taylor–Wiles 論證的整理，並接上既有的規則質數個案等形式化成果。Kevin Buzzard 在第一時間的技術評論中指出，這條較早期的路徑與 Imperial 團隊正在建構的現代證明不同；兩者最後都走向費馬大定理，但交付物、可讀性與可重用目標並不相同。

Anthropic 將成果稱為「第一份完整、可由電腦檢查的 FLT 證明」；本文只把這個「第一」狹義理解為完整一般形式的費馬大定理，而不是第一個重大定理形式化。Flyspeck 已完成克卜勒猜想的形式證明，Liquid Tensor Experiment 也在 2022 年用 Lean 完成主定理；FLT 的規則質數個案則在 2024 年已有完整 Lean 形式化。這次新增的是完整 FLT、11 天 campaign 與大規模 AI 代理的組合。

數量也要看口徑。Anthropic 的時間線把平台收尾時的總量寫成約 30,300 張 theorem cards／statement nodes，其中包含最終依賴樹外的敘述；離站重查的最終依賴樹則有精確 29,511 張卡。這不是同一欄數字互相打架，而是「平台曾產生」與「最後納入」的分母不同，也不代表 29,511 個彼此獨立的新數學發現。約 1,300 萬行同樣衡量程式體積，不直接等於數學洞見、可讀性或維護品質。

11 天不是從空白開始：真正工作的其實是一整個系統

Anthropic 描述的成功 campaign 歷時 11 天，但起點不是空白電腦。依官方時間線，第 11 天關閉的是 Prove2Me 根節點；全部 29,511 張卡的離站重編譯，以及組成單一 Lean 專案後的檢查，則在接下來兩天完成。底層已有 Lean、Mathlib、人類數學文獻、Imperial College London 的 FLT 專案，以及 flt-regular 對規則質數情況的成果。公開的歸屬清單辨識出 106 個含有直接取用或改寫上游 Lean 文字的檔案；這是檔案數，不能換算成人類與 AI 的貢獻比例，整體成果仍建立在 Mathlib 與人類數學文獻上。

中間層是研究者設計的 Prove2Me：它以有向無環圖拆分定理，讓代理平行工作並重用已完成節點。依 Anthropic 自述，這次另搭配 Claude Code-based multi-agent harness；大部分證明內容由 Claude agents 產生，Tianyi Peng 偶爾提供高層方向。因此「大致自主」比「完全沒有人類介入」更準確。

“what’s novel here is the verification—checking a mathematical proof as one would check a mathematical computation with a calculator.”

中文：「這裡的新意在驗證：像用計算機檢查運算一樣，檢查一份數學證明。」

Anthropic，〈Formalizing Fermat’s Last Theorem〉

這句話也點出 11 天應如何解讀：它是成熟模型、形式化函式庫、既有證明、專用編排平台與大量推論資源就位後，一次成功 campaign 的牆鐘時間。報告還說，最初數次嘗試失敗，最後成品約 7% 的非樣板程式來自那些嘗試。把所有前置研究與基礎設施抹掉，才會得到「AI 11 天從零完成」的錯覺。

Lean 的「通過」，到底保證了什麼？

一般程式測試只能抽查案例；形式證明則要交出一串能被小型核心驗證的證明項。Lean 核心不因為作者是 Claude 就放寬標準：每一步的型別必須成立，最後項目的型別必須正是目標命題。Lean 官方驗證指南再建議用 Comparator 把挑戰命題、允許公理與輸出證明隔離後重放，降低龐大專案用錯命題或偷帶依賴的風險。

Lean／Comparator 能強力確認	不能自動替人判定
最終形式命題是否真的被推出	自然語言敘述是否完整傳達同一件事
證明是否只使用列出的允許公理	中間定理名稱是否忠實反映內容
最終證明是否依賴 sorry 或額外公理	證明是否新穎、好讀、好維護
匯出後的證明能否由另一條檢查路徑接受	11 天的成本與工程方法是否可普遍複製

repository 報告最終檢查只列出 Lean 常見的 propext、Classical.choice 與 Quot.sound，沒有額外自訂公理、sorry、native_decide 或不安全宣告。Anthropic 另報告，經四個公開補丁修改的外部 Rust 檢查器 nanoda 接受輸出；這項結果的證據層級仍是公司自報。更重要的是，Buzzard 不只轉述公告，而是表示自己已編譯整個 codebase 並跑過 Comparator：「it checks out」。Buzzard 的獨立檢查，使「最終命題有完整、可機器檢查的證明」不再只是一項公司自述。

本文沒有宣稱在本機重現：README 估計完整建置需要約 67 GB 的 Lean 環境，產生的 C 檔可達約 220 GB，96 個 jobs 的建置耗時約 5 小時 32 分鐘、峰值記憶體約 153 GB；Comparator 又需約 14 小時 46 分鐘與更高記憶體。這裡採用的是公開 artifact、精確終點與 Buzzard 的獨立成品檢查紀錄，而不是把未執行過的指令包裝成「AlphaLab 實測」。

形式驗證很強，但不是「絕對不可能出錯」

2026 年 Lean 社群才公開處理過核心健全性漏洞；一份沒有 sorry 的 Collatz「反證」曾利用漏洞通過，外部檢查器當時也另有缺陷。Lean 維護者在後續檢討因此強調多重檢查。這不是說費馬大定理 repository 有已知問題：它使用含修補的 Lean 4.33.1，並採取 Comparator 加外部核心的強化流程。正確結論是「證據非常強」，而不是把任何軟體堆疊稱作形上學式的零風險。

關鍵誤讀：形式化完成，不等於理解完成

公開 README 主動提醒，這套程式是「為了被檢查，而不是為了被閱讀」而生成。機器可以確認某個形式敘述推出另一個敘述，卻無法只看函式名稱便判定「這真的是作者口中的 Mazur 定理」。若名稱與敘述衝突，Lean 檢查的是敘述；這個限制對最終那個簡單、可直接閱讀的費馬命題影響較小，對約三萬個中間節點的解釋、引用與重用卻很重要。

這也解釋了為什麼 Imperial 的 FLT 專案不會因這次發布而失去價值。截至 2026 年 9 月 5 日，Imperial 的頂層檔案仍明列 knownin1980s 與 sorryAx；Buzzard 團隊要做的不只有抵達終點，還包括把現代數論元件整理進 Mathlib、經過人類審查，並建立能讓人探索證明的動態文件。Anthropic README 則把其成果明確標為不維護、不接受貢獻的 research artifact。前者追求較可讀、可教、可維護的公共基礎設施；後者交付的是巨大、一次性、可驗證的另一條路徑。把 11 天與多年計畫直接排成效率競賽，是把不同產品當成同一產品。

如果把證明比作軟體，這次成果比較像「可完整建置、通過型別檢查並由另一套流程重放的大型 codebase」，而不是一套每個模組都有清楚命名、文件與維護承諾的函式庫。兩者都重要，只是解決的問題不同。

更值得注意的技術訊號：形式驗證開始成為可擴張流程

費馬大定理本身沒有因此變得更真；數學界原本就高度相信它。變化發生在驗證的供給：過往大型形式化專案往往需要專家團隊長期投入；這個案例顯示，專家可以設計目標與驗收條件，讓大量代理探索形式化路徑，再由核心拒絕不合法的步驟。若這種吞吐量能延伸到仍有爭議或細節缺漏的新研究，價值才會從「替經典結果加上憑證」升級成「提早找到文獻中的真缺口」。

但現有披露還不足以回答兩個關鍵問題。第一是經濟性：報告把模型描述為「大致相當於 Claude Fable 5.1」的內部研究模型，並提供約 60 億輸出 Token；這些資訊不能直接換算成零售 API 帳單。第二是可泛化性：Prove2Me 論文明確說明案例研究不是固定模型的控制實驗，模型能力與編排框架的貢獻仍糾纏在一起。一次壯觀成功，還不是穩定產線的良率報告。

AlphaLab 的判讀：別問 AI 是否「懂了」，先看交付物

我同意的部分

• 這是形式化工程的重要突破：終點命題清楚，artifact 公開，又有 Buzzard 獨立編譯並執行 Comparator，不只是一則只展示結果的 demo。
• 多代理拆解適合這類工作：形式證明有明確依賴圖與可執行驗收，比開放式「看起來合理」的研究任務更容易形成可靠回饋迴圈。
• 數學審查可能因此改變：AI 不必先創造新定理；只要能大幅降低把文獻送進 proof assistant 的成本，就可能讓隱含前提與缺口更早曝光。

我存疑的部分

• 自主性仍是系統層主張：模型、Prove2Me、Claude Code 框架、人工高層指導與既有形式化材料共同產生結果，不能只把功勞壓成「Claude 自己做完」。
• 程式量不是品質分數：1,300 萬行與約三萬個定理說明規模，不告訴我們其中有多少會被人類理解、維護或合併回公共函式庫。
• 成本與複製率仍待量化：這次披露的是單一成功 campaign；它不足以推估多題、固定設定下的成功率、總資源與失敗分布，也就不足以判斷一般研究團隊何時能使用同級流程。

接下來該看四個指標，而不是下一個更大的行數

1. 獨立重現：不同團隊能否從乾淨環境重建並重跑 Comparator／外部核心，留下可下載的完整 log。
2. 語意審查：抽樣檢查重要中間定理的名稱、文獻對應與強度，區分「型別正確」和「數學敘事正確」。
3. 公共重用：有多少基礎模組能被整理、審查並合併回 Mathlib，而不是永遠留在巨大專案內。
4. 單位經濟與良率：固定模型與框架後，公開每題總 Token、牆鐘時間、成功率和失敗重試，才能知道這是一次壯舉還是可持續流程。

如果你想判斷下一個「AI 完成大型研究任務」的消息，可以沿用同一套問題：目標是否可執行驗收？公開 artifact 是否對準原始命題？有沒有獨立重現？成功時間是否包含前置基礎設施？產出能否被人類接手？可再搭配 AI Evals 的證據分層與可驗收 Agent Harness，這比只比較模型名稱與 Token 數更接近真正能力。