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， 一個 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 請負責任地合併。

來源

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