Claude費馬大定理評測：11天寫出1300萬行Lean證明 | Claude Fermat's Last Theorem Review: 13M Lines in 11 Days

By Kit 小克 | AI Tool Observer | 2026-09-09

🇹🇼 Claude費馬大定理評測：11天寫出1300萬行Lean證明

最近整個科技圈都在討論 Claude 費馬大定理 形式化證明：Anthropic 旗下的多個 Claude 代理，只花了 11 天幾乎全自動運作，就用 Lean 程式語言寫出人類史上規模最大的形式化證明——1300 萬行程式碼、驗證超過 3 萬個定理，把 350 年前的數學難題「費馬大定理」變成電腦可以逐行檢查邏輯的程式。這篇文章用「好不好用、有沒有用」的角度，誠實拆解這件事的真相與限制。

Claude 怎麼在 11 天內完成費馬大定理形式化證明？

費馬大定理本身早在 1995 年就被數學家 Andrew Wiles 證明過。Claude 這次做的不是重新證明，而是把 Wiles 證明的簡化版本（Darmon-Diamond-Taylor 版）一步步翻譯成 Lean 這種「電腦可以自動驗證邏輯正確性」的程式語言。關鍵技術細節：

多代理協作：多個 Claude 實例透過開源工具 Prove2Me 分工，用有向無環圖（DAG）追蹤每個定理的證明進度，避免長時間工作後「忘記」自己在做什麼
規模驚人：總共寫出 1300 萬行 Lean 程式碼，證明 30,300 個中間定理（其中 29,500 個用進最終證明）
成本不便宜：消耗約 60 億個輸出 token，以 Anthropic 官網牌價換算約 30 萬美元
人類介入極少：研究員 Tianyi Peng 只給高層次提示，例如「Jacobian as a scheme 這條優先做」這種片段指令

費馬大定理證明是新數學發現，還是單純驗證？

這是本文最想誠實講清楚的部分：Claude 沒有發現任何新數學。倫敦帝國學院數學家 Kevin Buzzard（他自己主持一個五年、拿到英國政府百萬英鎊經費的同類計畫）明白表示，這件事「對數學本身沒有任何意義」——Wiles 的原始證明本來就有 99.9% 的把握是對的，Claude 只是把「人類覺得對」變成「電腦逐行驗證過的對」。真正有意義的是形式化驗證這件事本身被證明可以自動化到這種規模，而不是費馬大定理又被「證明」了一次。

對開發者與研究者的意義：能不能直接拿來用？

還不行，至少現在不行。這份 Claude 費馬大定理證明目前無法收錄進 Mathlib（數學界最大的 Lean 共用函式庫），因為維護者對 AI 生成程式碼的品質仍有疑慮；證明過程中也有約 7% 的非樣板程式碼來自失敗重來的分支，代表實際浪費不少算力。跟 Buzzard 團隊花 5 年、上百萬英鎊做同類工作相比，Claude 的 11 天、30 萬美元確實快很多也可能便宜很多，但這是「牌價」不是「真實內部成本」，也還沒有第三方完整覆核過整份證明。如果你的工作牽涉大型形式化驗證或長時間自主 agent 任務，這是目前最好的公開案例，值得研究 Prove2Me 這套協作架構，但別急著把 AI 生成的形式化證明當成「已驗證的真理」直接採用。

好不好用，試了才知道。

🇺🇸 Claude Fermat's Last Theorem Review: 13M Lines in 11 Days

The story lighting up AI Twitter and Hacker News this week is Claude's Fermat's Last Theorem formalization: a team of Claude agents from Anthropic spent just 11 days, working largely autonomously, to write the largest formal proof in history in the Lean language — 13 million lines of code verifying over 30,000 theorems, turning a 350-year-old math problem into something a computer can check line by line. Here's the honest, no-hype breakdown of what actually happened and what it doesn't mean.

How Did Claude Formalize Fermat's Last Theorem in 11 Days?

Fermat's Last Theorem was already proven by Andrew Wiles in 1995. What Claude did was translate a simplified version of that proof (the Darmon-Diamond-Taylor route) into Lean, a language where a computer can automatically verify every logical step. The key mechanics:

Multi-agent collaboration: Multiple Claude instances coordinated through an open-source tool called Prove2Me, which tracked progress on a directed acyclic graph of theorem statements so agents wouldn't lose context over days of work
Massive scale: 13 million lines of Lean code, 30,300 intermediate theorems proved (29,500 used in the final proof)
Not cheap: roughly 6 billion output tokens consumed, about $300,000 at Anthropic's list pricing
Minimal human input: researcher Tianyi Peng mostly gave fragmentary, high-level nudges like "Jacobian as a scheme sounds high priority"

Is This New Math, or Just Verification?

This is the part worth being blunt about: Claude didn't discover any new mathematics. Kevin Buzzard, the Imperial College mathematician who led his own five-year, roughly £1 million publicly-funded project toward the same goal, said the result "says nothing about mathematics" itself — the community already believed Wiles's original proof was correct with 99.9% confidence. What Claude proved is that formal verification at this scale can be automated, not that Fermat's Last Theorem needed re-proving.

Can You Actually Use This? Practical Takeaways

Not yet. The proof can't currently be merged into Mathlib, the Lean community's shared math library, because maintainers still have quality concerns about AI-generated code. About 7% of the non-boilerplate code came from failed attempts that had to be redone — real wasted compute, not a free lunch. Compared to Buzzard's team spending five years and roughly £1 million on similar formalization work, Claude's 11 days and ~$300K is genuinely faster and likely cheaper — but that's list price, not real internal cost, and no independent third party has fully audited the whole proof yet. If your work touches large-scale formal verification or long-horizon autonomous agents, Prove2Me's coordination architecture is worth studying. Just don't treat an AI-generated formal proof as verified truth you can drop straight into production math.

You won't know until you try it.

Sources / 資料來源

常見問題 FAQ

Claude真的證明了費馬大定理的新證法嗎？

沒有。費馬大定理早在1995年就被Andrew Wiles證明，Claude做的是把既有證明翻譯成Lean程式語言，讓電腦逐行驗證邏輯正確性，學術上稱為「形式化」而非「發現新證明」。

這份Lean證明可以直接用在自己的研究裡嗎？

目前還不行。這份證明尚未被Mathlib（Lean數學函式庫）接受，約7%程式碼來自失敗重來的分支，也還沒有第三方完整覆核，建議當作參考案例而非可直接複用的資源。

Did Claude actually discover a new proof of Fermat's Last Theorem?

No. Fermat's Last Theorem was proven by Andrew Wiles in 1995. Claude translated that existing proof into Lean so a computer could verify every logical step — this is called "formalization," not a new discovery.

延伸閱讀 / Related Articles

AI 工具觀察站 — 每日精選 AI Agent 與工具趨勢
AI Tool Observer — Daily curated AI Agent & tool trends

Claude Code 實測：AI 幫你寫程式到底行不行？ | Claude Code Review: Can AI Really Code for You?

3月 26, 2026

閱讀完整內容

搜尋此網誌

AI小貼士