Claude proved Fermat in 11 days. Verdict: SHIP IT.
Claude spent 11 days and about 6 billion tokens writing a 13-million-line Lean proof of Fermat's Last Theorem — the first end-to-end computer-checked one — while the mathematician who has been formalizing it since 2024 says it "tells us essentially nothing" mathematically and is thrilled anyway.
Claude spent 11 days and about 6 billion tokens writing a 13-million-line Lean proof of Fermat's Last Theorem — the first end-to-end computer-checked one — while the mathematician who has been formalizing it since 2024 says it "tells us essentially nothing" mathematically and is thrilled anyway. Same day: Go world No. 1 Shin Jin-seo beats KataGo 2–1 with a two-stone handicap. Verdict: SHIP IT.
What this video covers
- Claude formalizes Fermat's Last Theorem in Lean 4
- Chromium sandbox RCE (CVE-2026-85046), exploited in the wild, $1,000 bounty
- Shin Jin-seo beats KataGo with a two-stone handicap
Transcript
0:00 Fermat said his marvelous proof would not fit in the margin, and today Anthropic published the margin: thirteen million lines of Lean, five times the size of Mathlib, proving a theorem every mathematician already believed. It was ten to eleven in Tbilisi when Anthropic posted, so naturally I was awake. Yesterday Google shipped Chrome 152 with twelve security fixes, one of them a V8 bug already exploited in the wild, and paid the reporter a thousand dollars, which is less than the sedan we'll get to later.
0:26 Also yesterday, Mullvad said it is shutting down its public encrypted DNS on November 2nd and paying Quad9 to do it instead, and this morning the Rust React Compiler went native in Vite, while Hacker News discovered IBM Bob, an AI coding agent. Then Claude formalized Fermat's Last Theorem, and on the same front page a Korean grandmaster beat the strongest Go engine on Earth, so today humanity went one for two. In this video: what Claude actually proved, what it cost,
0:52 why the mathematician who spent his career on this says it changes nothing and is thrilled anyway, and how a human beat the machine at Go. It's Friday, September 4th, and this is The Daily Diff. Fermat's Last Theorem: no positive integers a, b, c satisfy a to the n plus b to the n equals c to the n for any n above 2. Fermat scribbled it in a margin around 1637 and died without showing his work, making him the first developer to close a ticket with works on my machine. A 1908 prize of 100,000 gold marks attracted 621 wrong
1:25 proofs in its first year, and Andrew Wiles finally got it in 1995, in 129 pages that took referees months to verify. Formalizing means rewriting that proof so Lean, a proof assistant, can check every step mechanically, and Kevin Buzzard at Imperial has led a human effort to do exactly that since 2024; the blueprint alone runs 86 pages. Anthropic researcher Tianyi Peng pointed dozens of Claude agents at it instead, on a platform called Prove2Me that keeps a DAG of theorem statements so agents know what to prove next, because without it the first
2:00 swarms lost track of who was proving what, which is what happens when your orchestration layer is regex with a marketing budget. Eleven days later the root node read PROVED: thirteen million lines of Lean, 29,500 intermediate theorems, about six billion output tokens from an internal model roughly comparable to Claude Fable 5.1. The build fails unless the proof rests on exactly Lean's three standard axioms: no sorry, no native decide, no cheating. Checking it is not cheap either: a
2:29 from-scratch build took five and a half hours on 96 cores and 153 gigabytes of RAM, and the theorem names are machine-generated, so the repo describes itself as written to be checked rather than read, which is also how I'd describe enterprise Java. Now the contradiction. Anthropic's post says Lean demonstrates correctness beyond a doubt. Kevin Buzzard, the man who got beaten to it, compiled the repo on a 500-gigabyte machine Anthropic lent him, confirmed it checks out, and then wrote,
2:56 quote, mathematically this work tells us essentially nothing. He was already 99.9 percent sure the theorem was true, and the proof adds no new math; what it shows is what autoformalization can do now, and that part he is genuinely excited about. He was given one million pounds over five years; Anthropic took eleven days, and a commenter's napkin math puts six billion output tokens at list price around 300,000 dollars, so the machine was cheaper, unless you count training the machine, which nobody does.
3:24 Best detail: the email arrived while he was at a music festival in Wales with one bar of 4G, from a name he had never heard of, so he wrote it off as a crank and read it a week later, which is the correct response to any subject line containing end-to-end formalization. Meanwhile, humans got one back. Shin Jin-seo, the world number one in Go, beat KataGo, the strongest open-source Go engine, two games to one in Seoul with a two-stone handicap, roughly the gap between a top professional and a rookie professional.
3:50 The decider was an 11.5-point win in 221 moves, holding a 99 percent win probability from mid-game on, and he took home 250 million won, about 170,000 dollars, plus a Genesis G90, so the bounty for beating a superhuman AI is 170 times Google's bounty for a Chrome sandbox escape. His explanation: early on he copied AI moves and lost; he won by building the board in his own style, which is the most useful advice about AI I have heard all year, and it came from a board game. Two more lines in the diff.
4:22 The Rust React Compiler from oxc is now native in Vite behind one flag; a 1,036-file codebase went from 14.3 seconds to 0.81 in the compile step, mostly by deleting Babel from package.json, which is also my skincare routine. And IBM launched Bob, an AI coding partner that greets you with Hi, I'm Bob, spawns subagents, modernizes mainframe code, and ships an analytics product called Bobalytics, so somewhere a bank is very excited and nobody read the license.
4:51 That is a lot of margin for one Friday; if you'd rather read this than hear me say it, the diff lands in your inbox every morning — free at the daily diff dot dev, link below. So, today's verdict: ship it. The kernel says yes, Buzzard says yes, the math did not change, but the way we check math just did. That's today's diff. I'm Niko from Axrisi.
5:09 Merge responsibly.
Sources
- Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
- The proof (Lean 4, Apache-2.0)github.com
- Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- HN threadnews.ycombinator.com
- KED Global — Shin defeats KataGowww.kedglobal.com
- HNnews.ycombinator.com
- Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
- NVDnvd.nist.gov
- Mullvad — shutting down public encrypted DNSmullvad.net
- Rust React Compiler native in Viteblog.master.dev
- IBM Bobbob.ibm.com
