Anthropic 於 2026 年 9 月 4 日公布一項數學形式化成果：該公司表示，Claude 約花 11 天、主要自主地以 Lean 撰寫出費馬最後定理的完整證明，並將其描述為「首個完整、經電腦檢查的費馬最後定理證明」。
先說結論：這不是 Claude 重新發現或重新解出費馬最後定理。Anthropic 明確指出，此案的創新在於驗證既有的數學論證，而非產生新的費馬最後定理數學結果。它的意義是把人類已知、但極其複雜的證明路線，轉譯成可由 Lean 與相關檢查流程驗證的形式化成果。
這也使「Claude 費馬最後定理」的討論焦點，從 AI 是否突然取代數學家，轉向另一個更實際的問題：AI 能否協助建立一條可機器檢查、可追溯的高可信度論證鏈？
Anthropic 公布了什麼？11 天、多代理與 1,300 萬行 Lean 程式碼
依據 Anthropic 的公告，Claude 約用 11 天完成這份 Lean 證明，專案產出約 1,300 萬行 Lean 程式碼，並由數十個 Claude agents 協作參與。
不過，「主要自主」不應被理解成一個單一模型在沒有任何人類指示或工程系統支援下獨力完成。Anthropic 的說法包含高階人類指示，以及 Prove2Me 與 Claude Code 的多代理工作流程。換句話說，這是一個由 AI agents、形式化工具與工程架構共同構成的研究系統成果。
| 外界常見說法 | 較精確的理解 |
|---|---|
| Claude 在 11 天「解出」費馬最後定理 | Anthropic 表示 Claude 在約 11 天內，將既有論證形式化為 Lean 可檢查證明；並非提出新的費馬最後定理數學結果。 |
| 完全由單一模型自動完成 | 成果涉及數十個 Claude agents、高階人類指示，以及 Prove2Me、Claude Code 的多代理工作流程。 |
| 「首個」已是無爭議的全球優先權結論 | 「首個完整、經電腦檢查的費馬最後定理證明」是 Anthropic 在公告中的描述；不宜延伸寫成已由外部單位裁定的跨系統全球優先權。 |
費馬最後定理早已成立，為什麼還需要 Claude 與 Lean？
公開專案 README 中的根定理可簡述為：對任意 n≥3 的正自然數 a、b、c，不會有 an + bn = cn 的情況。也就是說，正整數的 n 次方不可能形成這種等式。
既然數學界已有既有論證，形式化的價值並不在於改寫歷史結論，而在於把推理的每一個環節轉成機器可檢查的形式。對於跨越眾多定義、引理與抽象結構的長篇論證，這種做法可將「讀者是否在閱讀時漏掉某個細節」與「檢查器是否接受每一步形式推導」區分開來。
因此，這份成果更適合被理解為大型數學論證的形式化工程：它要求將原本供人類閱讀與理解的證明，拆解、表述並串接成可接受檢查的 Lean 程式碼。約 1,300 萬行的規模也說明，這不是把一篇短證明貼進證明助理就能完成的工作。
Claude 證明的是什麼？沿用 Frey、Serre、Ribet、Wiles 與 Taylor-Wiles 路線
公開庫的 PROOF-PATH.md 說明，該專案採取的論證路線連結 Frey、Serre、Ribet、Wiles 與 Taylor-Wiles 的工作，並主要依循 Darmon、Diamond、Taylor 的闡釋。
這一點相當關鍵。Claude 的角色不是憑空提出另一套費馬最後定理證法，而是把既有證明傳統所使用的論證路線，建構成可由形式系統檢查的版本。若把數學研究比喻為寫作，這不是另寫一部新小說；比較接近把一本高度複雜的原稿轉成具備嚴格語法、可逐段驗收的正式版本。
這樣的工作仍然困難。既有數學論文中的省略步驟、背景知識與讀者可自行補足的推理，在形式化環境裡都必須有明確表達。也正因此，AI 若能在長時間、多代理協作下參與此類工作，對未來數學工具鏈具有研究價值。
Lean 驗證到底保證什麼？又不能保證什麼？
從公開庫 README 的描述來看，根定理是在信任 Lean kernel，或 nanoda 與檢查工具的前提下，從 Lean 的三項標準公理推出。這提供了一個清楚的理解方式：形式化驗證不是抽象地宣告「絕對不會錯」，而是在特定形式系統、核心檢查器與執行工具可信的條件下，確認證明是否能被接受。
形式化檢查可帶來的價值
- 將根定理與支撐它的推導寫成可檢查的 Lean 成果。
- 讓讀者能取得公開程式庫，檢視定理陳述、論證路線與驗證相關說明。
- 把大型論證的正確性問題，部分轉化為明確的形式推導與工具檢查問題。
形式化檢查不應被過度解讀的地方
- 它仍有信任前提，包括 Lean kernel 或 nanoda 與檢查工具。
- 它不等於不需要人類可理解的數學闡釋；形式化版本與人類閱讀、理解論證的工作具有不同角色。
- 它不代表 AI 已經提出新的費馬最後定理數學結果。
- 它也不應被延伸為 Anthropic 的「首個」描述已完成跨所有形式系統的獨立優先權認定。
公開程式庫可以怎麼看？基礎建置與完整驗證要分開
Anthropic 已在 GitHub 公開專案庫釋出這份 Lean 研究成果。對想理解專案結構的研究者而言，README、根定理說明與 PROOF-PATH.md 是較適合的起點。
平台支援則需要精準區分。README 說明基礎建置可在 Linux 或 macOS 進行；但是，comparator 與 nanoda 腳本是 Linux 腳本。換言之，不能因為 macOS 可進行基礎建置，就推論完整 comparator 與 nanoda 驗證流程也同樣支援 macOS；更不應延伸到 Windows 支援的結論。
對一般讀者來說，公開程式庫最直接的價值是可檢視性：能看到定理如何被表述、專案選擇何種論證路線，以及其公開揭示的信任前提。至於在不同環境完整執行所有流程，則應以專案 README 與腳本的實際要求為準。
這和 Imperial College London 的 FLT 計畫有何關係？
Anthropic 表示其證明改編了 Imperial College London FLT 專案的部分內容。這不表示 Anthropic 已完成、結案或取代該計畫；Imperial College London 的公開 README仍將自身描述為進行中的多作者計畫。
理解這層關係很重要，因為大型形式化專案通常建立在長期的學術與社群累積之上。討論 Claude 的角色時，應同時看見既有形式化工作、原始數學論證，以及這次由 Anthropic 公開的多代理形式化成果。
這是否表示 AI 已能可靠從事原創數學研究？
僅憑這個案例，不能得出 AI 已能可靠完成原創數學研究的結論。Anthropic 自己將此成果定位為既有論證的驗證，而非新數學結果；因此，它較能支持的判斷是：在明確目標、形式化語言、工具檢查與多代理工程架構配合下，AI 可以參與極大型的形式化任務。
但這仍與「提出值得研究的新猜想」、「設計全新的證明策略」，或「在沒有嚴格形式化框架下穩定完成原創研究」是不同問題。未來更值得追蹤的，不只是模型能產生多少程式碼，而是它能否把生成結果持續放進可檢查、可審閱、可追溯的流程裡。
對 AI 數學與高風險研究審查的意義
這項成果最值得注意之處，是展示 AI 生成內容如何與機器檢查結合。若一個系統不只提出論證，還能把論證轉成可驗證的形式產物，研究團隊就有機會把重點從「是否相信模型的文字敘述」移向「是否能檢查其證據鏈」。
這個方向的潛在應用不只限於純數學。軟體驗證、晶片設計與其他錯誤代價很高的科研流程，都可能受益於更可檢查的推理與規格表述。不過，費馬最後定理專案同時提醒我們：可靠性並不是只靠模型生成，而是來自模型、形式語言、檢查器、執行環境與人類審閱共同構成的系統。
結論：Claude 的突破是把「已知」轉成「可檢查」
「Claude 費馬最後定理」最準確的表述是：Anthropic 表示，Claude 在高階人類指示與多代理工作流程下，約用 11 天將既有的費馬最後定理論證形式化為 Lean 可檢查證明，並公開相關研究成果。
它不是 AI 單獨重新解出這道數學名題，也不是不帶信任前提的絕對保證。它真正推進的是一種研究工作方法：讓極其複雜的推理不只存在於文字與專家理解中，也能以形式化方式接受工具檢查。
想進一步查看定理陳述、建置說明與論證路線，可直接閱讀 Anthropic 公開的 GitHub 專案庫與官方研究公告。
