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

本影片涵蓋的內容

• 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， 一個人工智能編碼代理。 然後Claude將費馬大定理形式化，而在同一個首頁上，一名 韓國圍棋大師擊敗了地球上最強的圍棋引擎， 所以今天人類的勝率是二分之一。 在本影片中：Claude實際證明了什麼，花費了多少，

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

1:25 證明，安德魯·懷爾斯最終在1995年完成， 共129頁，審稿人花了數月時間才驗證。 形式化意味著重寫該證明，以便Lean這個證明輔助工具， 可以機械地檢查每個步驟，帝國理工學院的Kevin Buzzard自2024年起就領導了一項人類 努力來完成這項工作；僅藍圖就有86頁。 Anthropic研究員Tianyi Peng則將數十個Claude代理指向它， 在一個名為Prove2Me的平台上，該平台維護一個定理的DAG（有向無環圖） 陳述，以便代理知道下一步要證明什麼，因為沒有它，第一批

2:00 群體會搞不清楚誰在證明什麼，這就是當你的 協調層是帶有市場預算的正則表達式時會發生的情況。 11天後，根節點顯示「已證明」：一千三百萬行的Lean程式碼， 29,500個中間定理，來自內部模型約60億個輸出token， 該內部模型大致可與Claude Fable 5.1媲美。 除非證明完全基於Lean的三個標準公理，否則建構會失敗： 不，抱歉，沒有原生決定，沒有作弊。 檢查它也不便宜：一個從頭開始的建構

2:29 花了五個半小時， 在96個核心和153GB的RAM上，而且定理名稱是 機器生成的，所以該存儲庫將自己描述為為了檢查而非閱讀而編寫， 這也是我會如何形容企業級Java。 現在是矛盾之處。 Anthropic的帖子說Lean無疑證明了其正確性。 被超越的Kevin Buzzard，在Anthropic借給他的500GB機器上編譯了該存儲庫， 確認了它的檢查結果，然後寫道：

2:56 引述：「從數學上來說，這項工作本質上沒有告訴我們任何東西。」 他已經有99.9%的把握該定理是正確的， 而且該證明沒有增加新的數學內容；它所展示的是自動形式化現在能做什麼， 而這部分他確實感到興奮。 他獲得了五年一百萬英鎊的資助；Anthropic只花了11天， 一位評論者的粗略計算顯示，按標價計算，60億個輸出token的花費是可觀的。 大約30萬美元，所以那部機器比較便宜， 除非你計入訓練機器的費用，但沒有人會這樣做。

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

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

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

4:51 對於一個星期五來說，這已經是很大的餘地了；如果你寧願閱讀這份內容而不是聽我說， 那麼The Daily Diff每天早上都會發送到你的收件箱——在thedailydiff.dev免費訂閱，連結在下方。 那麼The Daily Diff每天早上都會發送到你的收件箱——在thedailydiff.dev免費訂閱，連結在下方。 所以，今天的判決是：SHIP IT。 內核說可以，Buzzard說可以，數學沒有改變， 但我們檢查數學的方式剛剛改變了。 這就是今天的diff。 我是來自Axrisi的Niko。

5:09 請負責任地合併。

來源

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com