Claude費馬定理評測：11天形式化，非新證明 | Claude Fermat's Last Theorem Review: Formalized, Not New

9月 05, 2026

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

🇹🇼 Claude費馬定理評測：11天形式化，非新證明

Anthropic本週公布，旗下Claude AI耗時11天、幾乎全自動地把費馬最後定理（Fermat's Last Theorem）的證明轉換成電腦可逐行驗證的Lean程式碼，寫下1300萬行、證出3萬300個定理，其中2萬9500個用在最終證明裡。這是目前規模最大的形式化證明專案，但先講清楚：Claude沒有發現新數學，這件事本身也不是新聞裡常見的「AI解開百年數學難題」。

Claude到底做了什麼

費馬最後定理早在1995年就由數學家安德魯·懷爾斯（Andrew Wiles）證出，論文長達129頁，是數學史上公認的里程碑。Claude做的，是把懷爾斯的證明「翻譯」成Lean這套形式化證明語言，讓電腦可以逐一核對每一步邏輯是否成立——用Anthropic自己的比喻，這比較像「拿計算機檢查一道數學計算」，而不是自己想出新解法。

關鍵數字

耗時：11天，幾乎全自動運作
程式碼量：1300萬行Lean程式碼，是數學界主要證明庫Mathlib的5倍大
定理數：證出3萬300個定理，2萬9500個用於最終證明
算力：內部研究模型輸出約60億token
人力介入：僅來自研究者Tianyi Peng偶爾的高層指導

能在11天內完成，關鍵是一套叫Prove2Me的開源協作平台，由哥倫比亞大學研究者Tianyi Peng等人打造，用有向無環圖追蹤所有待證定理的狀態，並把「定理陳述」與「證明過程」拆成不同檔案加快編譯，還能用自然語言搜尋、重複利用已證出的定理。值得注意的是，Anthropic第一次嘗試形式化這個證明時失敗了，那次的程式碼只佔最終成果的7%左右——沒有Prove2Me，Claude一樣會迷失在專案狀態裡。

為什麼值得關注，但不用過譽

數學家原本預期，把懷爾斯證明完整形式化要花上數年人力。Claude把時間壓縮到11天，證明AI自動形式化的能力已經「夠可靠、可以被後續研究直接引用」，這是劍橋數學家Kevin Buzzard的評語。這對形式化數學社群是實質進展：以後有更多定理庫可以被AI快速驗證、擴充。但對一般讀者來說，別被「AI證出世紀難題」的標題誤導——真正的數學突破仍是1995年懷爾斯做的，Claude做的是把它變成電腦看得懂、能自動核對的版本。

好不好用，試了才知道。

🇺🇸 Claude Fermat's Last Theorem Review: Formalized, Not New

Claude, Anthropic's AI model, spent 11 days working largely autonomously to turn Fermat's Last Theorem into a fully machine-checked proof written in Lean, the formal verification language mathematicians use to have a computer confirm every logical step. The result: 13 million lines of Lean code and 30,300 proved theorems, 29,500 of which made it into the final proof. It's the largest formalization project on record — but it's not what most headlines are implying.

What Claude Actually Did

Fermat's Last Theorem was already proved by mathematician Andrew Wiles in 1995, in a 129-page paper that stands as one of the great achievements in math history. What Claude did was formalize — not discover — that proof: translate Wiles reasoning into Lean so a computer can verify each logical step is airtight. Anthropic own comparison: this is closer to checking a math computation with a calculator than inventing a new solution.

The Numbers

Time: 11 days, running largely autonomously
Code produced: 13 million lines of Lean — roughly 5x the size of Mathlib, math main proof library
Theorems proved: 30,300 total, 29,500 used in the final proof
Compute: about 6 billion output tokens from an internal research model
Human input: occasional high-level guidance from researcher Tianyi Peng — nothing more

The 11-day timeline was only possible thanks to Prove2Me, an open-source collaboration tool built by Tianyi Peng and collaborators at Columbia University. It tracks every pending theorem in a directed acyclic graph, splits statements from proofs into separate files to speed up compilation, and lets agents search and reuse already-proved theorems via natural language. Worth noting: Anthropics first attempt at this formalization failed outright, contributing only about 7% of the final code — without Prove2Mes scaffolding, Claude kept losing track of project state.

Why It Matters — Without the Hype

Mathematicians expected fully formalizing Wiles proof to take years of human labor. Compressing that to 11 days shows, in Cambridge mathematician Kevin Buzzards words, that AI autoformalization artefacts are now robust enough to be built upon — a real milestone for the formal-math community, who can now build directly on this work. But dont mistake this for a new theorem: the mathematical breakthrough happened in 1995. What Claude produced is a machine-checkable translation, not a discovery.

好不好用，試了才知道。

Sources / 資料來源

延伸閱讀 / Related Articles

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

搜尋此網誌

AI小貼士