# Claude 在 11 天內證明了費馬最後定理。判決：SHIP IT。

Published: 2026-09-07

Claude 花了 11 天和約 60 億個 token，寫出了費馬最後定理的 1,300 萬行 Lean 證明，這是第一個端到端經過電腦驗證的證明。而自 2024 年以來一直致力於形式化該定理的數學家則表示，它在數學上「基本上什麼都沒告訴我們」，但他仍然感到興奮。同一天：世界排名第一的圍棋選手申眞諝在讓兩子之下以 2 比 1 擊敗 KataGo。判決：SHIP IT。

Canonical: https://thedailydiff.dev/zh-TW/video/2026-09-04-fermat-lean/

## 本影片重點

- Claude 在 Lean 4 中形式化了費馬最後定理
- Chromium 沙盒 RCE (CVE-2026-85046)，已在野外被利用，獎金 1,000 美元
- 申眞諝讓兩子擊敗 KataGo

## 翻譯文字稿

譯自英文原版旁白。可用的音訊和字幕由 YouTube 控制。

0:00 費馬曾說他精妙的證明無法寫在頁邊空白處， 而今天 Anthropic 公布了這個空白處：一千三百萬行的 Lean， 是 Mathlib 的五倍大，證明了一個每個數學家都已經 相信的定理。Anthropic 發布時，提比里斯是晚上十點到十一點， 所以我自然醒著。 昨天 Google 發布了 Chrome 152，其中包含十二個安全修復， 其中一個是 V8 錯誤，已經在野外被利用，並支付了報告者 一千美元，這比我們稍後會提到的轎車還少。

0:26 同樣在昨天，Mullvad 表示將於 11 月 2 日關閉其公共加密 DNS， 並改由 Quad9 執行，而今天早上 Rust React 編譯器在 Vite 中原生運行，同時 Hacker News 發現了 IBM Bob， 一個 AI 編碼代理。 然後 Claude 形式化了費馬最後定理，而在同一個首頁上，一位 韓國圍棋大師擊敗了地球上最強的圍棋引擎， 所以今天人類的勝率是二分之一。 這部影片中：Claude 實際證明了什麼，花了多少錢，

0:52 為什麼那位為此投入畢生事業的數學家說這沒有改變任何事情，但 他仍然感到興奮，以及人類如何在圍棋上擊敗機器。 今天是 9 月 4 日星期五，這是 The Daily Diff。 費馬最後定理：沒有正整數 a、b、c 滿足 a 的 n 次方加上 b 的 n 次方等於 c 的 n 次方，其中 n 大於 2。 費馬在約 1637 年在頁邊潦草地寫下它，並在沒有展示其工作的情況下去世， 使他成為第一個用「在我的機器上運行良好」來關閉工單的開發者。 1908 年的 10 萬金馬克獎金吸引了 621 個錯誤的

1:25 證明在其第一年，而安德魯·懷爾斯最終在 1995 年證明了它， 這項證明長達 129 頁，裁判花了數月時間才驗證。 形式化意味著重寫該證明，以便 Lean（一種證明輔助工具） 可以機械地檢查每個步驟，而帝國理工學院的凱文·巴澤德自 2024 年以來一直領導著人類 努力這樣做；僅藍圖就有 86 頁。Anthropic 研究員彭天一反而將數十個 Claude 代理指向它， 在一個名為 Prove2Me 的平台上，該平台維護著定理的 DAG， 以便代理知道接下來要證明什麼，因為沒有它，第一個

2:00 集群就失去了誰在證明什麼的蹤跡，這就是當你的 編排層是帶有營銷預算的正規表達式時會發生的事情。 十一天後，根節點顯示 PROVED：一千三百萬行的 Lean， 29,500 個中間定理，來自一個 內部模型的大約 60 億個輸出 token，該模型大致與 Claude Fable 5.1 相當。 除非證明完全基於 Lean 的三個標準公理，否則構建將失敗： 不，抱歉，沒有原生決定，沒有作弊。 檢查它也不便宜：一個

2:29 從頭開始的構建花了五個半小時， 在 96 個核心和 153 GB 的 RAM 上，並且定理名稱是 機器生成的，因此該儲存庫將自己描述為寫作是為了檢查而不是 閱讀，這也是我會如何描述企業級 Java 的方式。 現在是矛盾之處。 Anthropic 的貼文稱 Lean 證明了正確性無可置疑。 凱文·巴澤德，那位被搶先一步的人，在 Anthropic 借給他的一台 500 GB 機器上編譯了儲存庫，確認其檢出無誤，然後寫道，

2:56 引述，「從數學上講，這項工作基本上什麼都沒告訴我們」。 他已經 99.9% 確定該定理是正確的， 而且這個證明沒有增加任何新的數學；它展示的是自動形式化現在能做什麼， 而那一部分他確實感到興奮。 他獲得了五年內一百萬英鎊的資助；Anthropic 只用了十一天， 一位評論者的粗略估計將 60 億個輸出 token 的成本按定價計算。 大約30萬美元，所以機器更便宜， 除非你把機器訓練也算進去，但沒人這麼做。

3:24 最棒的細節是：這封電子郵件是他當時在威爾斯的一個音樂節上收到的， 當時只有一格4G訊號，寄件人是他從未聽過的名字，所以他當成是惡作劇 一週後才讀，這才是對任何包含「端到端正式化」主旨行的正確反應。 包含「端到端正式化」的主旨行之正確反應。 與此同時，人類扳回一城。 圍棋世界第一的申真諝擊敗了KataGo， 這個最強的開源圍棋引擎，在首爾以兩子讓先的情況下，以二比一獲勝， 這大約是一個頂尖職業棋手和一個新秀職業棋手之間的差距。

3:50 決勝局是221手以11.5點獲勝，從中局開始就保持著 99%的勝率，他帶走了2.5億韓元，大約17萬美元， 加上一輛Genesis G90。因此，擊敗超人類AI的獎金是 Google對Chrome沙盒逃逸獎金的170倍。他的解釋是：早期他模仿AI的走法而輸了；他通過 模仿AI的走法而輸了；他通過以自己的風格佈局而獲勝， 這是我今年聽過關於AI最有用的建議，而且它來自一個棋盤遊戲。 這是我今年聽過關於AI最有用的建議，而且它來自一個棋盤遊戲。 差異檔中還有兩行。

4:22 來自oxc的Rust React編譯器現在在Vite中透過一個旗標原生支援；一個 1,036個檔案的程式碼庫在編譯步驟中從14.3秒降到0.81秒， 主要是透過從package.json中刪除Babel，這也是我的護膚程序。 主要是透過從package.json中刪除Babel，這也是我的護膚程序。 IBM推出了Bob，一個AI編碼夥伴，它會用「嗨，我是Bob」和你打招呼， 生成子代理，將大型主機程式碼現代化， 並推出名為Bobalytics的分析產品，所以某處的銀行非常興奮，但沒人讀授權許可。 興奮，但沒人讀授權許可。

4:51 對於一個週五來說，這是一個很大的收益；如果你寧願讀這份資料而不是聽我說， 那麼這個差異檔每天早上都會寄到你的收件匣—免費訂閱，網址是thedailydiff.dev，連結在下方。 那麼這個差異檔每天早上都會寄到你的收件匣—免費訂閱，網址是thedailydiff.dev，連結在下方。 所以，今天的判決是：SHIP IT。 核心說可以，Buzzard說可以，數學沒有變， 但我們檢查數學的方式剛剛變了。 這就是今天的差異檔。 我是Axrisi的Niko。

5:09 請負責任地合併。

## 來源

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com