Claude 用 11 天寫完費馬最後定理的電腦驗證證明：1,300 萬行程式碼，原本預期要花好幾年

一句話看懂：Anthropic 說，Claude 帶著數十個 AI 代理，大致自主地在 11 天內，把費馬最後定理的證明翻成電腦能逐行檢查的程式，共 1,300 萬行，原本預期要花好幾年。

先用白話講：「驗證證明」是什麼意思？

想像老師要批改一份 129 頁的數學作業。人類老師得從頭讀到尾，還要確認每一個「顯然可得」是不是真的顯然，只要有一個環節出錯，後面全部都可能是錯的。這種審查，一做就是好幾個月，甚至好幾年。

形式化就是把這份作業改寫成電腦看得懂的格式，每個推論一步都不能省，再交給一支「超嚴格的批改程式」逐行檢查。通過了，邏輯上就不會有漏洞。這支批改程式叫 Lean。

發生什麼事

Anthropic 在 9 月 4 日公布一項研究：

• 任務：把費馬最後定理（1995 年由 Andrew Wiles 證明）的證明，完整翻成 Lean 能驗證的版本
• 時間：Claude 大致自主地花了 11 天；官方說這項工作原本預期要花好幾年
• 規模：約 1,300 萬行 Lean 程式碼，證明了 30,300 個定理，最終證明用到其中 29,500 個
• 驗證：用 Lean 檢查，只用到 Lean 的三條標準公理，並確認結論與 Mathlib 對費馬最後定理的陳述一致
• 人的參與：人類只在偶爾下幾句高階指示，例如要優先處理哪個定理

重點：這不是 AI 發明新數學

這點很容易誤會。Anthropic 明確說，這次新穎的地方是驗證，就像用計算機檢查一道算式，不是產生新的數學內容。Claude 依照的是 Wiles 證明的一個簡化版本（出自 Darmon、Diamond、Taylor 的整理）。

給開發者的技術細節

對寫程式的人來說，比較值得看的是他們怎麼讓多個代理合作而不崩潰：

• 早期失敗：代理一開始很快就搞不清整個專案的狀態，也沒辦法有效合作，這些失敗的嘗試最後貢獻了約 7% 的非樣板程式行數
• 轉折：改用開源平台 Prove2Me（由 Anthropic 研究員 Tianyi Peng 與哥倫比亞大學團隊設計），搭配以 Claude Code 為基礎的多代理架構
• 定理依賴圖（DAG）：把所有定理陳述畫成一張有方向的圖，代理依此決定下一步做什麼，減少記憶退化，也讓多個代理可以平行作業
• 陳述與證明分檔：加快 Lean 的編譯，並降低資源消耗
• 自然語言描述：每個定理都附一段白話說明，方便搜尋與重複利用

Lean 的程式長這樣（這是自己舉的最簡單例子，不是官方內容）：

theorem my_add_comm (a b : Nat) : a + b = b + a := Nat.add_comm a b

全部過程用了約 60 億個輸出 token，使用的是 Anthropic 內部一個「大致相當於 Claude Fable 5.1」的通用研究模型。

我的看法

我自己用 AI 寫程式時，最大的課題一直是「怎麼知道它寫的是對的」。這則研究給我的感覺是：當成果可以被一個嚴格的自動檢查器驗證時，AI 就能放手跑很久。Lean 就是數學界的檢查器，我們寫程式的人手上則有型別檢查、單元測試和 CI。

另一個值得學的是它的分工方式：不是讓多個 AI 各寫各的，而是用一張共用的任務圖，讓大家知道誰做了什麼、下一步是什麼。這跟用多個代理平行寫專案時的「地基先行、契約凍結」是同一個道理。至於這是否代表 AI 能取代數學家，我覺得官方的說法已經很克制：它是減輕審稿負擔的工具，而不是取代人類理解。

名詞小辭典

• 形式化（Formalization）：把人看得懂的數學證明，改寫成電腦可以逐步檢查的格式。
• Lean：一種證明助理語言，要求每一步推論都寫清楚，由程式檢查是否有邏輯漏洞。
• Mathlib：Lean 社群共同維護的數學函式庫，收錄大量已形式化的定理。官方說這次 Claude 的證明大小超過它的 5 倍。
• 有向無環圖（DAG）：用箭頭表示先後依賴關係、而且不會繞回原點的圖，常用來排定任務順序。

資料來源

• Anthropic Research：Formalizing Fermat’s Last Theorem（2026-09-04）