2026 年 9 月 4 日，Anthropic 宣布完成一項 AI 數學里程碑：Claude 代理群在 11 天內，把費馬最後定理完整形式化為 Lean 程式碼，通過證明助手的機器檢驗。這個 1637 年提出、直到 1995 年才由 Andrew Wiles 以 129 頁論文證明的難題，如今變成一套 1,300 多萬行、只依賴 Lean 三條標準公理的完整證明。證明已放上 GitHub，任何人都可以自己跑一次檢查。
十一天、60 億個輸出 token
費馬最後定理說的是：當 n 大於 2 時，不存在三個正整數能滿足 aⁿ＋bⁿ＝cⁿ。Anthropic 的做法不是讓一個模型一口氣寫出答案，而是讓數十個 Claude 代理並行分工。背後是一個內部研究模型，能力大致相當於 Claude Fable 5.1，11 天內產出約 60 億個輸出 token，寫出 1,300 多萬行 Lean——是 Lean 數學函式庫 Mathlib 的五倍以上，總計證明 30,300 條定理，其中 29,500 條進入最終證明。證明路線採用 Darmon、Diamond 與 Taylor 在 1995 年對 Wiles 證明的簡化闡述，而非重新發明數學。
人類只給大方向
專案由 Anthropic 研究員 Tianyi Peng 發起，他在哥倫比亞大學的團隊打造了開放協作平台 Prove2Me：以 DAG 維護定理之間的相依結構、加速 Lean 編譯、支援搜尋與復用既有結果；外層再包一個以 Claude Code 為基礎的多代理 harness。人類輸入被壓到極低——Peng 只偶爾給出高層指示，例如「Jacobian 作為 scheme 聽起來優先級很高」。連失敗的嘗試都有剩餘價值：早期代理的產出貢獻了最終證明約 7% 的非模板行。Anthropic 還做了個對照展示：三個 Claude Max 訂閱帳戶上的代理，三天內形式化了維諾格拉多夫三素數定理。
Buzzard：檢查通過，但數學上「什麼都沒告訴我們」
受託驗證的是帝國理工學院數學家 Kevin Buzzard——他自 2024 年起領導社群的 FLT 形式化計畫，手上還有 EPSRC 五年 100 萬英鎊的補助。他自己編譯了這套證明、用比對工具確認敘述與 Mathlib 的 FLT 陳述一致，結論是「檢驗通過」，並稱其「除了數學公理之外不依賴任何假設」。但他同時潑了冷水：這套證明「忠實跟隨早期文獻，沒有加入任何新東西」，對數學本身「基本上什麼也沒告訴我們」。為了排除 AI 鑽 Lean 檢查器漏洞的可能，他手動讀完了全部約 100 行非數學程式碼。順帶一提，這項結果也宣告 Freek Wiedijk 的「百大形式化難題」清單全數完成。Claude 自己的工作日誌則留下了一行：「FLT root 顯示 Proved。歷史性時刻（有待複查）。」
對 AI 工程的意義
三件事值得記下。第一，長時程代理任務再次被驗證：11 天、數十個代理、千萬行程式碼，靠的不是更大的模型，而是環境工程——Lean 編譯器給出無曖昧的成功訊號、Prove2Me 維護共享任務圖譜、失敗產出還能被復用。第二，形式驗證正在變成 AI 程式碼品質的下個戰場：當「編譯通過」等於「數學上正確」，審查從逐行讀程式碼變成跑一次證明檢查器。第三，成本結構開始說得通：社群估算 60 億 token 約合數十萬美元 API 費用，對照 Buzzard 的五年學術補助，AI 形式化已從研究展示走向可用的生產力工具。正如 Buzzard 所寫：如果數千頁文獻能被 AI 群在 11 天內端到端形式化，未來「現代研究的形式化可能即時完成」。
參考來源
- Formalizing Fermat’s Last Theorem — Anthropic
- anthropics/fermats-last-theorem — GitHub
- FLT: Anthropic has beaten me to it — Xena Project
本文由 AI 協助自上述來源整理，經人工審核後發布。