Claude Proved Fermat's Last Theorem in Eleven Days — and the Mathematician Who Had Five Years and a Million Pounds to Do It Checked the Work Himself

Anthropic published a complete Lean formalization of Fermat's Last Theorem produced largely autonomously by dozens of Claude agents over 11 days: 13 million lines of code, 29,500 intermediate theorems, about 6 billion output tokens. Kevin Buzzard of Imperial College London, who holds a £1 million, five-year EPSRC grant to formalize the same theorem, compiled the repository himself, ran the comparator and inspected the code for hacks, and wrote that it 'checks out' but 'adds nothing' mathematically: the machine formalized the known proof rather than discovering anything new.