Claude 據稱 11 天完成費馬最後定理 Lean 形式化：重點不是「新證明」

Anthropic 表示，Claude 已產出費馬最後定理（Fermat’s Last Theorem，FLT）首個完整、端到端且可由電腦檢查的 Lean 形式化版本。這項說法最容易被誤解的地方是：Claude 不是重新發現了費馬最後定理的證明；它做的是把已確立的現代證明路線，轉換為 Lean 能夠逐步機械驗證的大型形式化成果。Anthropic 稱，這項工作由代理系統大致自主執行 11 天，產出約 1,300 萬行 Lean 程式碼。215

它究竟形式化了什麼？

費馬最後定理主張：當指數 (n\geq3) 時，方程式 (a^n+b^n=c^n) 沒有非平凡的自然數解。Mathlib（Lean 的重要數學函式庫）對此的表述是：若存在解，則 (a)、(b)、(c) 至少有一個為 0；這與「不存在正整數解」的常見說法等價。31

這個專案採用 Darmon–Diamond–Taylor 對 Wiles／Taylor–Wiles 證明策略的呈現方式，而不是另闢蹊徑提出新的數學證明。這一點很關鍵：在正式論文裡可以略過、以「由標準論證可得」帶過的環節，在形式化工作中都必須攤開，連同定義、前提、輔助結果及每一段銜接推理一併精確編碼。帝國理工學院既有的 FLT 形式化計畫也描述其路線為 Wiles／Taylor–Wiles 證明的現代變體。511

為何會膨脹到 1,300 萬行？

證明助理不接受「顯然可得」或「標準作法」這類省略。每一個推論都必須寫成系統可進行型別檢查的形式，每個結論也都要建立在已形式化的依賴之上。

Anthropic 表示，專案期間共產出約 30,300 個經電腦驗證的定理，其中約 29,500 個進入最終證明的依賴閉包；整個開發橫跨代數、幾何、調和分析與數論等領域。215

因此，「11 天」不能被解讀成 11 天就取代了費馬最後定理背後漫長的數學史。Anthropic 另稱，過程中約生成 60 億個 token。這代表大量候選證明、Lean 檢查後的錯誤修補，以及管理長時間形式化任務所需的工程工作，而不是短短 11 天憑空推導出一套人類未知的論證。5

關鍵不只模型能力，而是多代理人的外部協作

這項成果據稱並非單一模型一直把整部證明「記在上下文中」完成。Anthropic 指出，早期嘗試雖有進展，卻難以維持整個專案的共享狀態；後來成功的執行使用了以 Prove2Me 為基礎的工作框架。Prove2Me 是為協作式數學形式化而設計的平台。529

其核心組織方式是有向依賴圖：

• 節點代表尚待完成的定義、引理或定理；
• 邊則表示後續結果需要哪些前置結果；
• 代理人可挑選尚未完成、但對後續有用的任務，在 Lean 中完成證明，再讓其他代理人重複使用；
• 系統於是能從基礎元件逐步往上建構，最終抵達 FLT。

Prove2Me 將這種工作稱為啟動形式化「任務」，由代理人貢獻可重複使用的正式證明。29 實務上，依賴圖把一項冗長、脆弱的工作拆成眾多可檢查的子問題，並把專案記憶保存在模型單次執行之外。

「電腦驗證」到底保證了什麼？

Anthropic 稱，最終專案不含 sorry 占位符；在 Lean 中，sorry 可用來承認一個尚未真正證明的敘述。該成果據稱只依賴 Lean 的三項標準公理。5

這比 AI 寫出一篇看似令人信服的自然語言證明強得多。Lean 的核心會檢查每一個被編碼的步驟，確認它是否能從系統邏輯規則、公理與匯入的依賴中推出。Anthropic 也表示，已確認最終主張與 Mathlib 既有的 FermatLastTheorem 表述相符。531

不過，核心檢查有明確邊界：它驗證的是被形式化編碼的命題。人類仍須判斷其中的定義與中間命題，是否忠實表達原本想表達的非形式數學。因此，獨立編譯已釋出的成果，以及由專家檢閱其依賴鏈與語意對應，仍是評估這項宣稱不可或缺的步驟。

為何 Kevin Buzzard 稱之為「非凡」？

依 Anthropic 的報告，帝國理工學院數學家 Kevin Buzzard 將成果稱為「非凡的自動形式化成就」。21 意義不只是代理人能解幾題獨立的 Lean 練習，而是它們據稱組裝出一個層層相依、可重用、且涵蓋多個高階數學領域的形式化系統；以往人們預期，這類工作需要多年的人類協作。

若這種流程可重現、成本又能下降，數學形式化可能帶來幾項效益：

• 更嚴格的驗證： 系統可揭露散文證明中不易察覺的遺漏前提、無效轉換或定義不一致。
• 可重用的基礎設施： 一個引理完成形式化後，後續專案可直接匯入，並交由核心檢查，而非每次都從頭人工覆核。
• 作為同行評審的補強： 可機械檢查的證明有望減輕審查超長技術論證的負擔；但數學家仍必須評估其意義、重要性與策略。

這些是潛在好處，不代表數學判斷會被自動取代。一份形式證明可以在邏輯上成立，卻形式化了錯的問題；而 1,300 萬行程式碼與數十億 token 所反映的成本，也仍相當可觀。

解讀這項宣稱時，應把握的界線

這次 FLT 成果之所以是值得注意的 AI 輔助形式化基準，在於目標定理早已成立，而最終產物被設計為可供獨立檢查。它不應被說成 Claude 「新解」了費馬最後定理。

較準確、也更具影響力的說法是：Anthropic 報告指出，一個經由圖式任務分解協調的代理系統，已將一項重大且已知的證明轉換成前所未有規模的 Lean 開發，並把形式驗證用作持續回饋機制。21529

接下來真正重要的問題是：外部研究者能否重現建置、審核形式化內容是否保有原證明含義、重用其中元件，並在其他高深數學問題上得到相近成果。這些檢驗將決定它是一次性的工程壯舉，還是現代數學建構與驗證方式的持久轉變。