Anthropic宣佈，其AI模型Claude完成了費馬大定理的首個端到端、可由計算機完整檢查的形式化證明。這項成果以約1300萬行Lean程式碼、超過3萬個中間定理的形式呈現，最終證明使用了其中約29500個定理。這意味著，人類數學家能夠讀懂的證明，被徹底翻譯成了計算機能夠逐行檢查、沒有任何“這裡顯然”的形式化證明，將350多年的數學史濃縮進了龐大的程式碼庫中。

費馬大定理是數學史上最著名的難題之一，它指出對於任意整數n>2，都不存在正整數a、b、c使得aⁿ+bⁿ=cⁿ。自17世紀費馬提出這一命題以來，尤拉、勒讓德、庫默爾等一代代數學家不斷推進，卻始終未能給出完整證明。直到1993年，英國數學家Andrew Wiles首次公開宣佈證明，隨後又花費約一年時間與Richard Taylor合作修補，最終在1994年完成證明，困擾數學界350多年的命題才被攻克。

形式化證明是將數學證明轉化為計算機可驗證的格式，通常使用Lean等證明助手。普通數學論文寫給數學家看，人腦可以跳過許多步驟直接說“這裡顯然成立”，而形式化證明則要求每一步推導都從公理和定理合法地走一遍。Lean負責檢查這些推導是否合法。早在2024年，帝國理工學院的Kevin Buzzard等人就啟動了多年社群專案，準備用Lean完成費馬大定理的形式化，僅專案第一階段的技術藍圖就寫了86頁。

此次專案的核心人物是Tianyi Peng，他早年是資訊學競賽尖子，曾獲全國青少年資訊學奧賽選拔賽第八名，2017年從清華姚班本科畢業，2023年獲MIT博士學位。如今他是哥倫比亞大學助理教授、Anthropic研究員，長期聚焦強化學習、AI Agent與形式化工具。在他的主導下，多Agent協作系統被用於分工：有的負責補數學定義，有的專攻中間引理，有的沿著已有成果繼續推進更高層定理，還有Agent負責將不同部分重新拼回整個證明體系。

Anthropic透露，完整證明只依賴Lean的三個標準公理，他們還通過比較程式確認，Claude最終證明的定理陳述與Mathlib中的費馬大定理完全一致。專案初期，多Agent協作很快遇到了幾乎所有大型Agent系統都會面臨的問題——隨著工程規模擴大，Agent逐漸跟不上整個專案的狀態，協作效率下降。為此，Tianyi Peng及其哥倫比亞大學合作者搭建了Prove2Me協作系統，專門用於數學形式化。該系統通過一張“圖”讓Agent判斷哪些定理已證明、哪些還缺前置條件、下一步該攻哪個節點，同時將定理陳述和證明分開管理、加速Lean編譯，併為每個定理保留自然語言描述，方便不同Agent搜尋和複用已有成果。最終，Anthropic採用了Prove2Me+基於Claude Code的multi-agent harness方案。整個專案消耗約60億個輸出Token，內部使用的通用研究模型能力大致相當於Claude Fable 5.1。

Tianyi Peng在專案中更多隻是偶爾給出高層提示，比如某個方向優先順序更高、某個定理需儘快推進。負責審閱結果的Kevin Buzzard將其評價為一次“非凡的自動形式化成果”。如果如此規模、如此依賴複雜度的現代數學成果都能被AI自動搬進形式化系統，那麼過去極度依賴人工、推進緩慢的數學文獻形式化，可能第一次真正具備了大規模提速的條件。

與此同時，OpenAI也在推進類似方向。最新資訊顯示，GPT-6 Astra正在逐步向ChatGPT付費使用者開放，其中GPT-6 Pro面向Pro、Business和Enterprise計劃推出，Pro使用者還可在Chat、Work和Codex中使用Astra。Astra重點強化了推理、數學和Agent能力，預計將帶動更多數學、科研和Agent應用的出現。