The Daily Diff · Friday, September 4, 2026 · watch the episode
+ Claude formalizes Fermat’s Last Theorem
- Chromium sandbox RCE, exploited in the wild
+ Shin beats KataGo with a two-stone handicapFermat said his marvelous proof would not fit in the margin. Today Anthropic published the margin: 13 million lines of Lean, five times the size of Mathlib, proving a theorem every mathematician already believed. It was 22:50 in Tbilisi when Anthropic posted, so naturally I was awake.
The rest of the day, first
Chrome 152 (Thursday) shipped with 12 security fixes. One of them, CVE-2026-85046, a type confusion in V8, is already being exploited in the wild. Google paid the reporter $1,000, which is less than the sedan we’ll get to later.
Mullvad is shutting down its public encrypted DNS on November 2, 2026, after four years, and will fund Quad9 instead. Mullvad Browser defaults migrate automatically; manual DoH profiles do not.
The Rust React Compiler (oxc) is now native in Vite behind one flag,
react({ compiler: true }).IBM Bob made the Hacker News front page: an AI coding agent that says “Hi, I’m Bob!” and ships an analytics product called Bobalytics.
And on the same front page, a Korean grandmaster beat the strongest Go engine on Earth. Humanity: one for two.
Fermat’s Last Theorem, the short version
No positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n above 2. Fermat scribbled it in a margin around 1637 and died without showing his work — the first developer to close a ticket with “works on my machine.” A 1908 prize of 100,000 gold marks attracted 621 wrong proofs in its first year. Andrew Wiles finally proved 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. Kevin Buzzard at Imperial College has led a human effort to do exactly that since 2024; the project blueprint alone runs 86 pages.
What Claude did
Anthropic researcher Tianyi Peng pointed dozens of Claude agents at the problem instead, on a platform called Prove2Me that keeps a DAG of theorem statements so agents know what to prove next. Without it, the first swarms lost track of who was proving what and stopped collaborating — what happens when your orchestration layer is regex with a marketing budget. Their failed attempts still account for about 7% of the final lines.
Eleven days later the root node read PROVED:
13 million lines of Lean, over 5× the size of Mathlib
29,500 intermediate theorems used (30,300 proved)
about 6 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, nonative_decide
Checking it is not cheap either. A from-scratch lake build took 5 h 32 min on 96 cores with a peak of 153 GB of RAM; the comparator replay took 14 h 46 min; an independent Rust kernel (nanoda) checked 1,052,234 declarations with no errors. 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.
The contradiction
Anthropic’s post says Lean demonstrates a proof’s correctness “beyond a doubt.” Kevin Buzzard, the man who got beaten to it, compiled the repo on a 500 GB-RAM machine Anthropic gave him access to, confirmed it checks out, and then wrote: “mathematically this work tells us essentially nothing.” He was already 99.9% 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 £1 million over five years; Anthropic took 11 days. A commenter’s napkin math puts 6 billion output tokens at list price around $300,000, so the machine was cheaper — unless you count training the machine, which nobody does.
Best detail: the email arrived while Buzzard was at the Green Man 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. The correct response to any subject line containing “end-to-end formalization.”
Humans strike back
Shin Jin-seo, the world number one in Go, beat KataGo, the strongest open-source Go engine, 2–1 in Seoul with a two-stone handicap — roughly the gap between a top professional and a rookie professional. The decider was an 11.5-point win in 221 moves, holding a 99% win probability from mid-game on. He took home 250 million won (about $170,000) plus a Genesis G90, so the bounty for beating a superhuman AI is 170× 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. The most useful advice about AI I have heard all year, and it came from a board game.
Two more lines
Rust React Compiler in Vite: one team’s 1,036-file codebase went from 14.3 s to 0.81 s in the compile step (about 17×), full build 22.1 s → 9.3 s, mostly by deleting Babel from
package.json. Also my skincare routine.IBM Bob: agents and subagents, “Literate Coding,” a Bob Shell for CI, mainframe modernization packages, and Bobalytics. Somewhere a bank is very excited, and nobody read the license.
Verdict: SHIP IT — Kernel says yes. Buzzard says yes. The math didn’t change; how we check it did.
Sources
Anthropic, Formalizing Fermat’s Last Theorem — https://www.anthropic.com/research/formalizing-fermats-last-theorem
The proof repo (README, FinalCheck.lean, PROOF-PATH.md) — https://github.com/anthropics/fermats-last-theorem
Kevin Buzzard, FLT: Anthropic has beaten me to it — https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
HN: Formalizing Fermat’s Last Theorem (763 pts) — https://news.ycombinator.com/item?id=49568506
HN: Fermat’s Last Theorem in Lean 4 (repo) — https://news.ycombinator.com/item?id=49568697
KED Global: Go grandmaster Shin defeats AI KataGo — https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007
HN: Shin defeats KataGo with a two-stone handicap (467 pts) — https://news.ycombinator.com/item?id=49544762
HN: Actively exploited sandbox RCE in all Chromium versions (793 pts) — https://news.ycombinator.com/item?id=49570669
NVD: CVE-2026-85046 — https://nvd.nist.gov/vuln/detail/cve-2026-85046
Chrome Releases, Stable Channel Update for Desktop (Sep 3) — https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html
Mullvad: Shutting down our public encrypted DNS servers — https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead
HN: Mullvad DNS shutdown (474 pts) — https://news.ycombinator.com/item?id=49568579
Master.dev: React Now Rusted All The Way Out — https://blog.master.dev/react-now-rusted-all-the-way-out/
HN: The Rust React Compiler is now native in Vite (174 pts) — https://news.ycombinator.com/item?id=49567873
IBM Bob — https://bob.ibm.com/ · HN (333 pts) — https://news.ycombinator.com/item?id=49563851
Tweets: @AnthropicAI
HN front page for the day — https://news.ycombinator.com/front?day=2026-09-04
That’s today’s diff. I’m Niko from Axrisi — merge responsibly.
YouTube · thedailydiff.dev · forward this to the intern who deployed on Friday.