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，研究人員可以繼續逐行審查其結構與正確性。
