Anthropic published the first complete computer-checked formalization of Fermat's Last Theorem on September 4, 2026 — a task the mathematical community had expected to take years of coordinated human effort — after Claude wrote 13 million lines of Lean proof-assistant code in 11 days using a multi-agent platform that solved the fundamental problem of how AI agents share mathematical state across long, complex projects.
The result does not represent new mathematics. Andrew Wiles proved Fermat's Last Theorem in 1995; the underlying argument remains his. What Claude produced is a formalization — a translation of that 129-page proof into a language a computer can verify line by line, algorithmically and without ambiguity, eliminating any reliance on a human referee's judgment. Kevin Buzzard, the Imperial College London mathematician who has been leading a multi-year community project to formalize the same theorem, reviewed the result and said it proves the theorem "with no assumptions other than the axioms of mathematics."
That distinction — verification, not discovery — is important. It is also, for the long-term practice of mathematics, possibly more important than another discovery would have been.
To read more, click here.