Anthropic 於 2026 年 9 月 4 日宣布，其 AI 模型 Claude 在 11 天內幾乎完全自主地完成了數學史上最著名的難題之一——費馬最後定理（Fermat’s Last Theorem, FLT）的完整電腦可驗證形式化證明。Claude 在此過程中寫下了 1,300 萬行 Lean 程式碼，證明 29,500 個中間定理，最終生成被 Lean 證明助手確認無誤的閉合證明鏈。
核心成就
史上最大的 Lean 證明
Claude 透過 多代理協作框架，在 Prove2Me 平台上動員數十個 Claude 代理協同工作。產出的證明規模驚人：
- 1,300 萬行 Lean 程式碼——超過 Mathlib（Lean 社群核心數學庫）的 5 倍
- 30,300 個定理（29,500 個用於最終證明）
- 消耗約 60 億輸出 Token（使用與 Claude Fable 5.1 相當的通用研究模型）
- 採用的證明路徑繼承自 Darmon、Diamond 與 Taylor 簡化版 Wiles 證明
人類參與極為有限
堪稱里程碑的是，人類在此過程中的參與僅限於偶爾的高層指導。Anthropic 研究員 Tianyi Peng 僅給出類似「Jacobian as a scheme sounds high priority」、「push Mazur theorem to be done soon」的粗略指令。Claude 代理自主決定目標拆解、定理排序與程式碼生成。
技術細節：為何 Lean 形式化如此困難
形式化驗證的挑戰
與人類可讀的數學證明不同，Lean 證明助手要求每一步推理都明確無誤。對於 FLT 這樣的複雜證明：
- Wiles 於 1995 年發表的原始證明長達 129 頁，由數學家花了數月審查才確認
- 數學社群原定需要 數年時間 來完成形式化——僅描述初始階段的「藍圖」就長達 86 頁
- Lean 不接受任何「顯而易見」的跳躍，每個代數操作、每個同構映射都必須明確編碼
Prove2Me 平台的關鍵作用
Claude 最初多次嘗試失敗——代理雖能獨立完成子任務，但很快失去對專案狀態的全局視野，協作效率驟降。失敗的努力約貢獻了最終證明中 7% 的非模板行數。
轉折點來自切換到 Prove2Me 平台，這是由 Tianyi Peng 與其 Columbia 大學團隊開發的開放協作形式化平台。Prove2Me 透過三項機制解決了多代理協作的核心難題：
- 有向無環圖（DAG）結構：維護定理陳述的依賴圖，讓代理自行決定下一步該證明的子目標
- 分離定理陳述與證明：將定理陳述與證明程式碼分置不同文件，顯著加速 Lean 編譯
- 自然語言檢索：為每個定理配備自然語言描述，降低代理重複勞動
產業與學術意義
1. AI 形式化能力質變
Anthropic 的這一成果標誌著 AI 在自動形式化驗證領域的重大跨越。Kevin Buzzard 教授（Imperial College London）評論道：
如果 FLT 的自動形式化現在已成為可能，那麼我們已朝自動形式化現代數學文獻邁出了一大步。這樣的技術將催生新工具，根除當前數學語料中的錯誤，並減輕審稿人的負擔。
2. 數學審查流程的未來
隨著 AI 生成的數學結果數量激增，傳統的同行審查流程面臨前所未有的壓力。Claude 的成果展示了一條可行路徑：任何 AI 生成的數學證明都應附帶可被電腦自動核驗的形式化版本。這可能從根本上改變數學期刊的審查流程——從耗時數月的人工審查，轉向以電腦核驗為基礎、人工判讀為輔的雙軌制度。
3. 對亞洲數學研究的啟示
對於香港與亞洲的數學研究社群而言，此事件的意義不僅在於技術突破，更在於研究流程的潛在革命。形式化證明工具在 AI 輔助下變得前所未有的易用，數學家可以：
- 將繁重的驗證工作交由 AI 代理完成，專注於概念創新
- 利用 Lean 的即時反饋快速迭代證明策略
- 通過 Prove2Me 這類平台建立跨機構協作的形式化專案
4. 消費者級 AI 的潛力
Anthropic 研究人員還做了一項有趣的實驗：使用三個個人 Claude Max 訂閱方案協作形式化 Vinogradov 三質數定理（Hardy-Littlewood Circle Method 的應用），結果僅用 3 天 即完成。這意味著即使是消費級的 AI 訂閱，在合適的協作框架下也能完成重大數學形式化工作。
關於費馬最後定理
費馬最後定理指出，當整數 n > 2 時，方程式 aⁿ + bⁿ = cⁿ 無正整數解。1637 年，費馬在書本空白處寫下「我發現了一個絕妙的證明，可惜此處空白太小寫不下」。這個猜想困擾了數學界長達 358 年，直到 1995 年 Andrew Wiles 爵士才給出首個正確證明。2026 年的今天，Claude 在 11 天內完成了 Wiles 證明的完整形式化——數學史上最漫長的等待之一，迎來了最快的電腦驗證。
本文信息來源：Anthropic 官方研究報告「Formalizing Fermat’s Last Theorem」（2026 年 9 月 4 日）、Kevin Buzzard 評論、Hacker News 社群討論。