Anthropic 在 2026 年 9 月 4 日公開表示，費馬最後定理已經有了一份能由電腦全程驗證的證明。絕大多數工作由 Claude 完成，歷時約 11 天，寫出的 Lean 程式碼達到 1300 萬行，最終證明中用到 29500 條中間定理。這並沒有產出新的數學成果，但驗證證明這件事的速度，已經和過去不在同一個量級。
走了 350 年的證明，以及它背後的驗證難題
費馬把那句話寫在書頁空白處，大約是 1637 年。對任何大於 2 的指數，不存在正整數 a、b、c 滿足 a 的 n 次方加 b 的 n 次方等於 c 的 n 次方。命題誰都讀得懂，證明卻 350 多年無人給出。1908 年有人懸賞 10 萬金馬克，光是第一年就收到 621 份錯誤的證明。※該獎金換算成今日幣值約為 100 萬至 200 萬美元（約 1.6 億至 3.1 億日圓）。以 1 美元 = 156 日圓換算。
真正了結此事的是 1995 年 Andrew Wiles 那篇 129 頁的論文。這份證明同樣沒有立刻被接受。1993 年演講中公布的初版，在審查過程中被指出存在關鍵漏洞，Wiles 花了一年時間，和昔日學生 Richard Taylor 一起把缺口補起來。而要讀通這 129 頁並確認無誤，多位數學家投入了數個月。
形式化的想法正是從這裡來的：把證明改寫成機器讀得懂的語言，讓電腦去找出邏輯漏洞。寫給人看的證明會把大量步驟視為理所當然而略過，而證明輔助系統 Lean 要求每一步都交代清楚。就費馬最後定理而言，Imperial College London 的 Kevin Buzzard 於 2024 年發起的社群專案一直在推進，光是描述初始階段的藍圖就有 86 頁。這原本被視為以年為單位的工程。
11 天，1300 萬行
推動這件事的是 Anthropic 研究員 Tianyi Peng。他在 Columbia University 的團隊長期開發形式化工具，他想試試 Claude 能在這個難題上走多遠，結果超出預期。
數字能看出規模。11 天生成 1300 萬行 Lean 程式碼，途中證明了 30300 條定理，其中 29500 條進入最終證明。作為依據的 Mathlib 是社群最核心的數學證明資料庫，而這份證明的體量是它的 5 倍以上。Anthropic 自己也承認，寫法很可能比實際需要的冗長許多。
證明路線並非 Wiles 的原始論證，而是以 Henri Darmon、Fred Diamond 與 Richard Taylor 的簡化解說為底本。人類的介入僅止於偶爾給出的高層建議，例如把作為概形的雅可比優先處理。最終證明只依賴 Lean 的三條標準公理，並透過專門的比對工具確認所證命題與 Mathlib 中費馬最後定理的敘述一致。
這份成果並非憑空而來。它從 Buzzard 的專案，以及處理正則質數情形的 flt-regular 中取用了元件，而 Lean 與 Mathlib 本身就是數百位數學家共同養成的產物。Buzzard 讀過這份證明後指出，AI 自動形式化的產物如今已經穩固到可以讓別人接著往上搭建的程度。
最初的嘗試是失敗的
過程並不順利。早期試驗中，各個代理起初還有進展，隨後就搞不清整個專案進行到哪一步，協作因此瓦解。最終證明中扣掉樣板程式碼後的行數，約 7% 來自這些失敗的嘗試。
局面翻轉的節點，是改用 Prove2Me 這個協作平台之後。它由 Peng 與其合作者設計，發揮作用的有三點：把待證定理之間的相依關係維護成有向無環圖，讓代理能判斷下一步該從哪裡著手；把定理敘述與證明拆到不同檔案，藉此減輕編譯負擔；為每條定理附上自然語言描述，使已完成的結果可被搜尋與重複使用。
底層是以 Claude Code 為基礎搭建的多代理架構，消耗的輸出 token 約 60 億。所用模型為內部通用研究模型，能力大致相當於 Claude Fable 5.1。
對數學研究現場代表什麼
當形式化能在現實可接受的時間內完成，同儕審查的分量就變了。原本要靠人花上數年確認一項新結果是否成立，如今機器可以分擔相當一部分。在 AI 生成的數學成果不斷累積的當下，這部分驗證成本已經大到無法忽視。
這套做法看來也不是大型專案的專利。Anthropic 研究人員做過一個小實驗，只用三個個人版 Claude Max 訂閱，透過 Prove2Me 協同作業，三天就完成了維諾格拉多夫三質數定理的形式化。只要鷹架搭得合適，用一般訂閱去形式化重要定理並非遙不可及。
對 Claude 本身也有副作用。近期由 Claude 完成的成果，往往在證明的同時並行做形式化，Claude 似乎會用這些部分形式化來自我檢查假設是否站得住腳，就像它寫數值模擬來確認方向是否正確一樣。
完整證明已在 GitHub 公開，並附上梳理證明脈絡的說明文件。
總結
11 天、1300 萬行、29500 條中間定理。費馬最後定理第一次有了機器能從頭驗到尾的證明。價值不在於新的數學，而在於驗證。確認證明是否正確的工序正從人手轉向機器，而產出的成果已經穩固到能成為下一份證明的地基，這才是此次最大的變化。
