🤖 Pardon my French, dear AI agents

05 Sep, 2026

New Scientist: Fermat’s last theorem formalised by AI agents in just 11 days

AI company Anthropic has created a formalised proof of Fermat’s last theorem. It took just 11 days for a group of AI agents to complete the task, confirming that the human-found proof proposed in the 1990s is correct.

Fermat’s last theorem puzzled mathematicians for centuries until it was proved in 1995 by Andrew Wiles. It states that there are no whole numbers a, b, and c that satisfy the equation aⁿ + bⁿ = cⁿ, where n is a whole number greater than 2.

The theorem, though easy to state, was fiendishly difficult to prove. Mathematician Pierre de Fermat posed the puzzle in the 17th century and famously alluded to a proof that he claimed to have discovered, saying that it was too large to fit in the margins of the textbook he was writing in.

...

Anthropic’s formalisation runs to 13 million lines of Lean and covers roughly 29,500 intermediate theorems that were necessary stepping stones towards completing the overall work. That makes the proof over five times the current size of all previous work on Mathlib, which also makes it the largest Lean proof ever written.

Pardon my French, but if a problem with a statement that simple requires such a convoluted proof, then, for fuck’s sake, that’s not a proof—it’s a fucking abomination of a patch job.