摘要： Anthropic 表示 Claude 代理群用 11 天把費馬最後定理形式化成 Lean，產出超過 1,300 萬行程式並由證明助手檢核。Kevin Buzzard 確認結果只依賴數學公理，但也說它忠實跟隨既有文獻，對數學本身沒有新貢獻。這個案例的重點是環境工程與機器驗證，而不是新的數學證明。
2026 年 9 月 4 日，AI 在數學領域跨過一道里程碑：Anthropic 表示，旗下一群 Claude 代理只花了 11 天，就把費馬最後定理整條命題轉譯成 Lean 程式碼，並交由證明助手以機器方式逐項檢核完畢。這道 1637 年出現的猜想，要等到 1995 年才由 Andrew Wiles 用一篇 129 頁的論文拿下；如今它以 1,300 多萬行程式的面貌存在，除了 Lean 的三條標準公理之外，不倚賴任何其他前提。整份證明已公開在 GitHub 上，想親自確認的人可以自行執行檢查。
產出規模：11 天、約 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 萬英鎊的補助。Buzzard 親手編譯了這套證明，再用比對工具確認其敘述與 Mathlib 的 FLT 陳述一致，結論是「檢驗通過」，而且「除了數學公理之外不依賴任何假設」。不過他也當頭潑了冷水：這份證明「忠實跟隨早期文獻，沒有加入任何新東西」，對數學本身「基本上什麼也沒告訴我們」。為了排除 AI 鑽 Lean 檢查器漏洞的可能，他把全部約 100 行非數學程式碼人工讀過一遍。這項結果還附帶一個效果：Freek Wiedijk 的「百大形式化難題」清單就此全數完成。Claude 自己的工作紀錄裡則留下了這麼一行：「FLT root 顯示 Proved。歷史性時刻（有待複查）。」
這件事對 AI 工程的意義
有三件事值得記下來。第一，長時程代理任務再度通過實測：11 天、數十個代理、上千萬行程式碼，真正撐起成果的並非更大的模型，而是環境工程——Lean 編譯器給出毫無模糊空間的成功訊號、Prove2Me 維護共享的任務圖譜、失敗的產出也還能回收再利用。第二，形式驗證正在變成 AI 程式碼品質的下一個戰場：當「編譯通過」就等於「數學上正確」，審查的重心便從逐行讀程式碼，轉為跑一次證明檢查器。第三，成本結構開始說得通：社群估算 60 億 token 約合數十萬美元的 API 費用，拿來對照 Buzzard 那筆五年的學術補助，AI 形式化已經從研究展示走向可用的生產力工具。正如 Buzzard 所寫：如果數千頁文獻能被 AI 群在 11 天內端到端形式化，未來「現代研究的形式化可能即時完成」。