新聞

Anthropic公布費馬最後定理形式化（Formalizing）成果，以Claude Code為基礎的多代理系統花11天，第一次完成可由Lean證明助理從頭到尾檢查的形式化證明。整項工程產生約1,300萬行Lean程式碼，完成30,300項定理證明，最終證明使用29,500項。

該成果並非提出新的費馬最後定理解法，而是把既有證明改寫成電腦能逐步檢查的形式。Claude採用Darmon、Diamond與Taylor整理的Wiles證明路徑，補齊人類數學論文常省略的定義、推導與中間步驟，讓Lean逐項確認證明是否成立。

費馬最後定理形式化原先預估需要數年，Kevin Buzzard自2024年在Imperial College London推動費馬最後定理形式化計畫，光是描述初期工作範圍的技術文件就有86頁，而Claude產生的Lean程式碼規模，超過Lean主要數學函式庫Mathlib的5倍。

Anthropic一開始直接讓多個Claude代理協作，但代理逐漸無法掌握整體進度，工作也難以銜接。團隊後來改用Columbia University研究團隊開發的Prove2Me，以圖狀結構記錄各項定理的前後相依關係，讓代理依照目前進度挑選下一項證明工作，並把定理敘述與證明拆開處理，減少Lean編譯需要的運算資源。

Prove2Me也替每項定理保存自然語言說明，讓不同代理搜尋及重複使用已完成的證明。整項工程使用約60億個輸出Token，採用的內部研究模型能力大致相當於Claude Fable 5.1。

完成的證明通過Lean檢查，只使用Lean的3項標準公理，Lean的Comparator工具確認費馬最後定理敘述與Mathlib版本一致。完整Lean程式碼與證明說明公開於GitHub，成果利用Mathlib與Imperial College London既有的形式化工作。