Claude 在 11 日內以 Lean 形式化費馬最後定理
Anthropic 表示，Claude 寫出 1,300 萬行 Lean 程式碼，完成首個經電腦檢查的費馬最後定理完整證明。
文章目錄 · 11
Anthropic 於 9 月 4 日宣布，Claude 已完成首個經電腦檢查的費馬最後定理完整證明。該公司表示，數十個 Claude 代理在 11 日內大致自主地工作，生成約 1,300 萬行 Lean 程式碼，並證明了 30,300 個定理，其中約 29,500 個出現在最終證明中。
這並非傳統數學意義上的費馬最後定理新證明。Andrew Wiles 與 Richard Taylor 已於 1990 年代完成獲接受的人類證明。Claude 所做的，是把文獻中既有的論證路徑翻譯成一種形式語言，讓電腦可以檢查當中的邏輯步驟。
這個分別很重要。這項成果幾乎沒有為費馬最後定理是否為真增加新知識，卻顯示一個 AI 系統可以形式化一整套原本預計需要專家花多年完成的高等數學。帶領另一個形式化項目的倫敦帝國學院數學家 Kevin Buzzard，編譯了 Anthropic 的程式碼並運行其比較器檢查。他表示該證明通過檢查。
一、Claude 正式證明了甚麼
費馬最後定理指出，當整數指數 \(n\) 至少為三時，沒有正整數 \(a\)、\(b\) 及 \(c\) 滿足 \(a^n+b^n=c^n\)。這個陳述很簡單，但已知證明依賴涉及橢圓曲線、模形式、伽羅瓦表示、變形理論、代數幾何及數論的複雜結果。
Anthropic 的程式庫直接以 Lean 的自然數表達最終定理。其陳述採用正自然數 \(a\)、\(b\) 及 \(c\)，連同 \(n \geq 3\)，並證明該方程不可能成立。另一項最終檢查則由這個定理推導出 Mathlib 現有的費馬最後定理陳述。
該論證遵循 Frey、Serre、Ribet、Wiles 及 Taylor–Wiles 的工作，尤其是 Henri Darmon、Fred Diamond 及 Richard Taylor 於 1995 年的闡述。它利用費馬方程假設解與一條 Frey 橢圓曲線之間的聯繫，然後應用模性及降階結果以得出矛盾。
Buzzard 指出此構造的一項重要細節。Anthropic 基於 Wiles 的路徑處理質數指數 \(p \geq 17\)。完整結果納入先前已形式化的正規質數工作，以補足其餘情況。不過，所得的 Lean 定理仍涵蓋所有至少為三的自然數指數。
這項成果亦依賴大量較早的人類工作。Anthropic 表示，它改編了倫敦帝國學院 FLT 項目、flt-regular 項目及 Mathlib 的材料。其署名檔案列出 106 個包含首兩個項目材料的檔案，以及 23 個重現 Mathlib 文字的檔案。因此，這項成就是由 AI 主導，對現有形式化生態系統所作的整合與擴展，而非在沒有既有形式數學基礎下獨立創作的 1,300 萬行程式碼。
二、多代理系統如何管理這項證明
Anthropic 起初發現，Claude 代理能證明個別結果，卻會失去對整個項目的掌握。代理重複工作，未能有效重用已完成的定理，而且隨着證明規模擴大便停止協調。失敗嘗試仍佔最終非樣板程式碼約 7%。
成功的一次運行使用了 Prove2Me，這是一個由哥倫比亞大學 Tianyi Peng 及其合作者開發的開放協作形式化平台。Prove2Me 將項目表示為由定理陳述組成的有向無環圖。代理可以選擇未完成的節點、證明先決條件，以及重用圖中其他地方產生的結果。
該平台亦將定理陳述與其證明分開。這種設計降低重新編譯成本，並讓系統能夠修改或替換一項證明，而不會擾亂每個依賴它的陳述。附於定理節點的自然語言描述，為代理提供另一種搜尋逐漸擴大的程式庫及識別有用依賴關係的方法。
一個基於 Claude Code 的多代理框架，在這次 11 日運行期間協調數十個代理。據報人類數學輸入僅限於偶爾提供高層次優先事項，例如引導代理研究 Jacobian，或要求它們完成一個與 Mazur 工作相關的定理。內部日誌記錄，根定理於 8 月 18 日證明完成。
Anthropic 報告指，該次運行消耗約 60 億個輸出 token。它使用一個內部通用研究模型，僅稱其大約可與 Claude Fable 5.1 相比，因此確切模型及配置並未公開。公司尚未披露該項目的金錢成本或運算成本。
完成的開發在其可瀏覽文件中包含 29,511 個定理頁面及 1,450 個定義模組。Anthropic 在整次更廣泛的運行中計算出 30,300 個可由電腦驗證的定理，包括最終依賴路徑最終不需要的結果。
三、證明如何經過檢查
形式證明只有在定理陳述、獲允許的假設及驗證過程均受控制時才有價值。Anthropic 的程式庫將項目固定於 Lean 4.33.1 及 Mathlib 4.33.0，並包含多個檢查層次。
首先，項目由零開始建置。其 60,475 個模組由 Lean 核心檢查。最終定理恰好依賴三項標準 Lean 公理：命題外延性、經典選擇及商的健全性。分散式證明模組不包含未完成的 sorry 佔位符、新宣告的公理、不安全程式碼、原生決策捷徑或外部實作。
其次，項目使用 Lean Comparator，把已證明的定理與一份只基於 Mathlib、另行提供的挑戰陳述作比較。此檢查旨在確認解答證明相同命題、沒有使用未獲批准的公理，並獲核心接受。比較器返回接受判決。
第三，一個名為 nanoda 的獨立 Lean 核心實作檢查了匯出的環境版本，並無錯誤地接受了 1,052,234 項宣告。Anthropic 對 nanoda 套用了四個修補程式：一個用於進度輸出，三個用於加速定義相等性搜尋。程式庫表示，當中沒有任何一個改變或削弱型別規則。
Buzzard 提供了最具相關性的外部確認。他在一部 96 核心機器上編譯程式碼，並親自運行比較器。他形容該程式庫超過 1,340 萬行，並表示其編譯時間接近 Lean 數學程式庫的 20 倍。
重現每項檢查是可行的，但對硬件要求很高。Anthropic 文件記載的建置，在 96 個平行工作下耗時 5 小時 32 分鐘，記憶體峰值為 153 GB，Lean 建置使用約 67 GB，另產生最多 220 GB 可移除的生成 C 檔案。其比較器運行耗時 14 小時 46 分鐘，記憶體峰值為 230 GB。為第二個核心匯出環境時，產生了一個 37.8 GB 檔案。
這些檢查證明，在至少一個檢查核心及周邊驗證工具正確的前提下，確切的形式陳述可由列出的公理推導而來。它們不會自動證明每個中間定理由機器生成的名稱，都準確描述其數學含義。Anthropic 透過一份證明路徑文件處理這項限制，該文件把主要數學步驟對應至其確切 Lean 陳述。
四、AI 輔助數學有何改變
在這項成果之前，費馬最後定理是 Freek Wiedijk 長期列出的 100 項著名定理形式化挑戰中尚餘的一項。倫敦帝國學院項目於 2024 年開始，獲得五年資助，最初目標是把定理歸約至 1980 年代末已知的結果。其項目材料指出，完整形式化將需要翻譯數千頁非形式數學。
Anthropic 的證明反而端到端地抵達最終定理。Buzzard 強調，這不會令他的項目變得多餘：帝國學院的工作正為 Mathlib 開發可重用、人類可讀的補充內容，並遵循一條較現代的證明。Anthropic 將其程式庫標示為不會維護、亦不接受貢獻的研究成果。
因此，實際進展在於吞吐量。Claude 的代理跨越代數、調和分析、幾何及數論，組裝形式定義與證明，其規模超過 Mathlib 程式碼行數五倍以上。結果顯示，基於圖的代理系統能保存依賴關係，並在規模大至超出單一模型上下文可容納的形式化工作中協調作業。
這項證明亦展示了 AI 生成數學的驗證路徑。語言模型可以產生帶有令人信服文字、但不正確的自然語言論證；然而，Lean 會拒絕無法通過型別檢查的證明項。另行控制的定理陳述及比較器，進一步降低代理透過暗中削弱或改變問題而成功的風險。
這個機制不會消除對數學家的需要。人類仍須決定一個形式陳述是否捕捉預期概念、評估成果的重要性與闡述方式，以及維護可重用程式庫。不過，它可以將邏輯步驟的詳盡檢查由人類審稿人轉移至證明輔助器核心——前提是定義、定理陳述及受信任的驗證邊界均經獨立檢視。
常見問題
Claude 是否發現了費馬最後定理的新證明？
否。它把 Frey–Serre–Ribet–Wiles–Taylor–Wiles 文獻中既有的論證路徑形式化，讓 Lean 可以檢查每一個邏輯步驟。
結果是否經過獨立驗證？
Kevin Buzzard 編譯了公開程式碼並運行 Lean Comparator，表示它通過檢查。程式庫亦記錄了 Lean 與獨立 nanoda 核心成功完成的檢查。
哪個 Claude 模型產生了這項證明？
Anthropic 未有公布確切的公開模型名稱。它形容該內部通用研究模型大致可與 Claude Fable 5.1 相比。
研究人員能否重現驗證？
可以，程式碼及指示均以 Apache 2.0 授權公開。完整重現需要大量硬件，包括在某些驗證階段需要數百 GB 記憶體。
這個 1,300 萬行程式庫是否全屬全新、由 AI 撰寫的數學？
否。AI 代理生成並整合了大部分開發內容，同時建立於 Mathlib，以及倫敦帝國學院 FLT 和 flt-regular 項目較早的開源形式化工作之上。
參考來源
Share