Anthropic 於近日宣佈，旗下 AI 模型在基本自主運行11天后，成功完成了對費馬大定理（FLT）的首個端到端、經過計算機檢查的 Lean 形式化證明。這項工作並非由 AI 重新發現該定理的數學證明，而是將已有數學證明轉換爲 Lean 證明助手能夠逐步驗證的形式。Lean 是一種用於編寫和驗證形式化數學證明的證明助手，能夠通過計算機檢查證明中的邏輯步驟。

在這一過程中，Claude 生成了約1300萬行 Lean 代碼，並證明了約3.03萬個定理，其中約2.95萬個中間定理最終被納入費馬大定理的完整證明。整個證明由 Lean 完成檢查，僅使用了 Lean 的3條標準公理。這項工作的目標是將英國數學家安德魯 · 懷爾斯於1995年完成的費馬大定理證明進行形式化。費馬大定理指出，當整數指數 $n$ 大於2時，不存在滿足 $a^n + b^n = c^n$ 的正整數 $a$、$b$、$c$。懷爾斯的原始證明長達129頁，其正確性在發表前經歷了數月人工覈查。

數學形式化的難點在於，人類數學證明通常會省略大量被認爲顯而易見的推導步驟，而 Lean 需要明確驗證每一個邏輯環節。此外，數學家長期以來會引用大量尚未被形式化的既有數學成果，因此將完整證明轉換爲計算機可驗證形式通常需要投入大量時間。Anthropic 此前曾預計費馬大定理的形式化工作可能需要數年時間。

image.png

此次項目由 Anthropic 研究人員 Tianyi Peng 發起。Claude 並非由單個智能體完成全部工作，而是通過多智能體協作完成概念定義、中間定理證明以及更復雜命題的推導。項目使用了由 Peng 及其哥倫比亞大學合作者開發的 Prove2Me 平臺，用有向無環圖記錄待證明的定理及其依賴關係，並支持多個 Claude 智能體並行工作。最終證明遵循了 Darmon、Diamond 和 Taylor 對懷爾斯證明的簡化版本。人類研究人員提供的數學輸入主要是少量高層次指令，例如確定某些數學對象或定理的優先級，具體證明過程則主要由 Claude 完成。

整個項目消耗了約60億個輸出 Token，使用的是一個與 Claude Fable5.1大致相當的通用內部研究模型。最終生成的證明規模超過 Mathlib 這一主要數學證明庫的5倍。Anthropic 特別強調，此次成果的重點並不是 AI 獨立提出了新的費馬大定理證明，該定理早在1995年已由懷爾斯證明，此次工作的創新之處在於利用 AI 大規模自動完成證明形式化，並由 Lean 對最終結果進行計算機驗證。

Anthropic 認爲，如果類似的自動形式化技術能夠擴展到更多現代數學成果，就有望降低數學研究中驗證新證明的人工成本。隨着 AI 生成數學成果的數量增加，爲面向人類閱讀的數學證明同時提供形式化版本，未來可能成爲常見做法。此次項目的完整 Lean 證明已經公開在GitHub上。同時，數學家 Kevin Buzzard 對該證明進行了審閱，並認爲這項自動形式化成果顯示，AI輔助形式化大型數學成果已經取得重要進展。