Claude formalized Fermat's Last Theorem in 11 days
Anthropic says a team of Claude agents produced the first complete, machine-checked formalization of Fermat’s Last Theorem — and Kevin Buzzard, the Imperial College London mathematician who has spent years on the same problem, has already compiled the result and confirmed it checks out. Also today: React’s compiler has gone Rust-native, and one real codebase got most of its build time back.
Claude just closed the last open problem on formal mathematics' most famous benchmark list. Working on Prove2Me, a platform built by Anthropic researcher Tianyi Peng's group at Columbia, a swarm of Claude agents ran largely on their own for eleven days and proved Fermat's Last Theorem in the Lean proof assistant: 29,511 theorems, roughly 13 million lines of Lean, resting on nothing but Lean's three standard axioms with no unproved placeholders anywhere. Humans occasionally nudged priorities but wrote no mathematics beyond the one-line statement of the goal. The build was then re-run from scratch off-platform and cross-checked by two independent verifiers — the Lean Focused Research Organization's comparator tool, which confirmed the statement proved is exactly the elementary one fixed in advance, and nanoda, a separate reimplementation of Lean's kernel written in Rust, which accepted every declaration.
The proof follows the 1990s Wiles–Taylor–Wiles route as set out by Darmon, Diamond and Taylor, so it breaks no new mathematical ground — and Kevin Buzzard, who holds an EPSRC grant to formalize the modern proof, is blunt about that. Writing hours after the announcement, he noted he was given £1 million to run his project over five years while Anthropic took eleven days, that he compiled the repository and ran comparator on it himself and "it checks out," and that this was the final unformalized entry on Freek Wiedijk's 20-year-old list of 100 formalization challenges. He also flagged the real caveat: the result covers primes at or above 17, though that gap is closed by earlier work formalizing FLT for odd regular primes. What matters isn't the theorem. It's that eleven days of agent labor now buys you an end-to-end formalization that used to be a career, and the refereeing bottleneck for AI-generated mathematics just got a lot cheaper to relieve.
React's compiler went Rust-native, and one real codebase got its build back. The oxc project shipped official support for the Rust port of React Compiler on August 4, and Vite's React plugin followed with opt-in native support in v6.1.0 — which means the Babel-based compiler, and its Babel plugin dependencies, can come out of your build entirely. Andrew Patton's team moved a 1,036-file React Router codebase over and watched the compiler portion of their build drop from 14.3 seconds to 0.81 seconds, about 17 times faster; the overall build, which includes plenty that isn't the compiler, still went from 22.1 seconds to 9.3 seconds. For anyone running agent-assisted development, where GitHub Actions minutes have quietly become a real line item, that compounds fast.
The speed is almost the less interesting half. The Rust compiler also fixes several patterns that made the old Babel version silently skip components — conditional logic inside try/catch blocks, reassigning a destructured prop used in a nested closure, computed object property keys — which in Patton's app meant seven more functions getting optimized. It still bails on a throw from inside a try block and on logical assignment operators, but the fixes now land on a compiler you're actually running. The underrated win is consistency: when your linter and your build run the same compiler version, you stop getting components that sail through lint unoptimized because the two tools disagreed about what the compiler supported.
What to watch: whether Mathlib takes any of the infrastructure Anthropic built — deformation rings, Néron models, Tate curves — as human-led contributions, rather than the proof itself, which by Claude's own assessment "is not meant for upstreaming as it stands."
Would you trust a machine-checked proof you can't read, or does verification only count if a human can follow the argument? Tell us in the comments.
