Anthropic 於 2026 年 9 月 4 日發表研究文章，表示 Claude 已完成 Fermat 大定理（Fermat’s Last Theorem，FLT）的完整 computer-checked proof。根據 Anthropic 的說法，Claude 用大部分自主的方式工作約 11 日，把一個由人類讀者理解的長篇數學證明，轉換成 Lean proof assistant 可以逐步檢查的形式。
這項成果的背景不是 AI 突然找到一個人類未知的初等證明。Andrew Wiles 早在 1995 年已發表 FLT 的第一個正確證明；今次的主題是 formalization，即把已有的數學推理改寫成電腦能夠演算法式核查的形式。Anthropic 自己也把新意放在 verification，而不是把它包裝成另一個 Riemann hypothesis 式的嶄新數學結果。
Anthropic 表示，Claude 在過程中寫了約 1,300 萬行 Lean，並完成 30,300 個中間 theorem，其中 29,500 個最後被納入證明。這個規模很能說明形式化的工作量：人類證明會省略被認為明顯的步驟，但 Lean 要求每個邏輯連接都能被檢查。文章又表示，最終 proof 超過 Mathlib 主要社群數學庫五倍以上。
背後的工作流並不是一個單一聊天視窗。Anthropic 說，數十個 Claude agents 透過 Prove2Me 協作，先以 directed acyclic graph 管理 theorem statements，再平行處理定義、子定理和證明。這種設計針對了長任務常見的記憶退化和狀態失焦問題：代理需要共享一張可搜尋、可重用、可追蹤的證明圖。
Lean 的價值在於它會檢查形式邏輯，而不是因為模型說「已證明」就接受結果。Anthropic 表示，完成的 proof 已由 Lean 核查，使用 Lean 的三個標準公理；文章也提到 Kevin Buzzard 查看過 proof，以及另一個 comparator 確認 theorem statement 與 Mathlib 的 FLT statement 相符。這些是重要的可追溯訊號，但目前仍應把它視為 Anthropic 的研究發布和開放 proof artifact，讀者仍要按自己的標準重跑、審閱及獨立驗證。
對 AI agent 研究而言，這個案例顯示瓶頸正在由「模型能否產生一段看似合理的推理」轉向「代理能否維持長期狀態、拆分依賴、處理失敗並交付可核查的 artifact」。Anthropic 說，早期嘗試曾因 agents 失去專案狀態而失效，最後靠共享 DAG、編譯加速和 theorem search 才讓多代理流程穩定下來。
對數學社群來說，formalized proof 不會取代人類可讀的 exposition，也不會自動回答研究結果是否值得相信的全部問題；它更像一個可重跑的邏輯底座。當 AI 產出更多證明或研究假設時，能否同時交付 Lean、Rocq 或其他 proof assistant 的形式化版本，可能會成為降低 referee 負擔和捕捉錯誤的重要工作流。
這宗新聞最值得記住的不是「AI 證明了 Fermat 大定理」這句容易誤讀的標題，而是 agentic research 開始把協作、形式化、編譯和驗證放進同一個長任務。數學新意、工具可核查性、研究者審閱和獨立重現，仍然是四件不同的事；把它們分開，才不會把一個很有價值的驗證工程誤報成 AI 取代數學家。
