Claude 以多代理協作完成費馬最後定理的 Lean 形式化，公開 1,300 萬行證明

Anthropic 公開一套以 Lean 4 寫成的費馬最後定理形式化證明。據[技術報告](https://www.anthropic.com/research/formalizing-fermats-last-theorem)，數十個 Claude 代理透過 Claude Code 多代理框架工作 11 天，共產生約 1,300 萬行 Lean、證明 30,300 個中間定理，最終使用其中約 29,500 個；推理模型是能力約等同 Claude Fable 5.1 的內部研究版本，整項工作消耗約 60 億個輸出 token。

早期嘗試因代理逐漸失去專案狀態、無法有效重用成果而失敗。團隊改用 Prove2Me，把目標拆成有向無環圖：代理可挑選尚未完成的定理、搜尋既有結果，並將定理宣告和證明分檔編譯，避免修改一個節點便重新處理整座證明樹。[Prove2Me 論文](https://arxiv.org/abs/2608.28433)把這種架構定位為可同時容納人類與代理的協作式形式化平台。

公開的[證明儲存庫](https://github.com/anthropics/fermats-last-theorem)固定使用 Lean 4.33.1 與 Mathlib 4.33.0，並禁止 `sorry`、新增公理、`unsafe` 等逃生路徑。Lean 核心完成全量建置後，`comparator` 再確認最終命題與 Mathlib 版本相同；另一個以 Rust 實作的 nanoda 核心也檢查逾 105 萬個宣告。證明只依賴 Lean 的三項標準公理。

這並非 Claude 發現新的費馬最後定理證法，而是把 Frey、Serre、Ribet、Wiles 與 Taylor–Wiles 路線轉成機器可驗證成品。重現成本也不低：官方完整建置曾使用 153 GB 記憶體，comparator 約需 15 小時、峰值達 230 GB。核心檢查能保證型別正確，卻不能判斷中間定理名稱是否忠實表達數學意義；下一步應觀察獨立團隊能否重建結果，以及這套編排方法能否在較少 token 與人工提示下處理其他大型數學文獻。