Anthropic 於 2026 年 9 月 4 日公開研究成果：Claude 以約 11 天，將費馬最後定理的既有證明轉寫成 Lean 程式，並完成電腦檢查。9 月 5 日的新報導讓這項成果受到關注，但研究執行早在 8 月就已完成。這次新聞是成果公開，不是 Claude 今天突然解出一道沒人會解的數學題。
不是重新證明，而是讓每一步能被檢查
費馬最後定理說的是：當整數次方大於 2 時，找不到三個正整數，讓前兩者的該次方相加等於第三者的該次方。Andrew Wiles 的證明早已在 1995 年發表；這次沿用既有數學路線，把人類論文中的推理翻成 Lean 能理解的形式語言。
差別在於，數學文章可以省略專家認為顯然成立的步驟，電腦卻需要完整的定義與推導。公開程式庫列出了建置檢查與定理比對：不只讓程式跑完，還要確認證明使用的公理，以及最後得到的命題，確實對應 Mathlib 裡的費馬最後定理。
多個 AI 怎麼一起完成這麼大的工程？
Anthropic 表示，數十個 Agent 合作產生約 1,300 萬行 Lean 程式。關鍵工具 Prove2Me 會整理定理之間的依賴關係，讓 Agent 看見哪些結果已完成、下一步需要什麼，並搜尋可重用的定理。它處理的是大型合作的進度與依賴，不只是要求模型一直往下寫。
帝國理工學院數學家 Kevin Buzzard 也公開說明，他自行編譯程式並執行比對，結果通過。不過他提醒，能通過形式檢查的龐大程式，和容易閱讀、維護、供其他研究重用的數學函式庫，仍是不同成果；人類的理解工作不會因此消失。
不是訂閱 Claude 就能一鍵重現
這次使用的是能力約相當於 Claude Fable 5.1 的內部研究模型，搭配多 Agent 工具，研究者仍偶爾給予高層次指示。官方披露約用了 60 億個輸出 tokens，沒有公布可直接核對的實際帳單。因此不能把它說成一般帳號免費可用，也不能拿公開 API 單價硬算成這次研究成本。
想看細節的人已能取得公開程式碼，但儲存庫明確標示為研究成果，不持續維護、也不接受貢獻。對開發者而言，這是可研究與核對的實驗產物，不是具有長期支援承諾的產品 API，更不是把任意題目貼進聊天框就保證得到正確答案。
真正值得注意的是「答案能不能查」
這項成果對一般 AI 使用者的啟示，是把「生成答案」和「檢查答案」分開看。流暢的解釋不等於正確；這次有明確定理、可公開檢查的程式與形式驗證工具，才讓成果具有可核對的基礎。它展示 AI 能協助處理龐大的驗證工程，但不代表所有專業領域都已經具備同樣完整的檢查條件。
