Anthropic 表示，Claude 已完成費馬大定理的首個完整形式化證明。這不是重新發現這一定理，而是將既有證明轉寫為計算機可逐行核驗的邏輯代碼。公司稱，這項工作耗時 11 天，最終生成約 1300 萬行內容。
形式化證明的意義，在於將數學論證寫成機器可檢查的語言。傳統論文證明往往需要同行長期複核，一旦中間某一步有漏洞，修補過程可能持續數月甚至數年。費馬大定理由英國數學家 Andrew Wiles 於 1995 年完成證明，但要把這套證明完整轉成可機檢版本，一直被視為高強度工程。
11 天完成長期項目目標
倫敦帝國理工學院數學家 Kevin Buzzard 從 2024 年起推動相關項目，目標同樣是將 Wiles 的證明轉寫到 Lean 證明助手。按原計劃，這項工作需要長期協作，資金已安排至 2029 年。
Anthropic 表示，Claude 在此任務上提前達成了同類目標。Buzzard 審閱後表示，這份證明能在不依賴額外假設的情況下成立，也就是僅基於數學最基本的公理系統完成驗證。
由多代理並行完成
根據 Anthropic 的介紹，哥倫比亞大學研究人員 Tianyi Peng 的團隊讓多個 Claude 代理並行工作，分別負責編寫定義、證明較小的結論，再逐步拼接成更大的證明結構。人工干預較少，主要是給出階段性優先順序。
早期的進展並不順利。Anthropic 表示，部分代理一度無法共享已完成的內容，也會重複工作。隨後，團隊使用名為 Prove2Me 的工具，為各代理提供統一的任務清單和文件組織方式，並保留自然語言備註，幫助它們複用彼此的結果。
- 支撐性定理超過 3 個萬
- 總消耗達到數十億 token
- 最終證明約 1300 萬行
重點在於可驗證，而非新定理
本次成果的重點不在於發現全新的數學命題，而在於將已有的重大證明轉化為可由計算機逐步驗證的版本。隨著數學論文和 AI 生成內容的增加，人工逐條檢查證明的成本也在上升，因此形式化工具更受關注。
Anthropic 還表示，此證明的規模已超過數學界常用共享庫 Mathlib 的 5 倍以上。完整文件已上傳至 GitHub，研究人員可繼續逐行審查其結構與正確性。