Anthropic said this week that an internal research model, working largely on its own through a multi-agent setup, produced the first complete, computer-checked proof of Fermat's Last Theorem in the Lean programming language. The run took 11 days, generated 13 million lines of Lean code, and proved roughly 30,300 supporting theorems along the way. Kevin Buzzard, the Imperial College mathematician who has led the human effort to formalize the same proof, reviewed the result and called it a genuine step toward automatically formalizing large parts of the mathematical literature.

The mechanics explain how a task mathematicians expected to take years got compressed into under two weeks. Dozens of Claude agents worked in parallel against a shared dependency graph on Prove2Me, an open collaborative platform, each deciding which sub-theorem to tackle next and building toward the final result the way a large team of specialists might divide up a huge proof by hand. Lean itself, not a person, verified every step using only its three baseline axioms — which is what makes the claim checkable rather than just an impressive transcript.

The model is commodity compute, the verifier is what makes it trustworthy

It's worth being precise about what made this possible, and what it doesn't prove more broadly. None of the underlying infrastructure was built for this run: Buzzard's own multi-year formalization project, the Mathlib community library the proof builds on, and Prove2Me itself all predate it and were necessary for it to work at all. It's also a domain with an unusually clean advantage for this kind of automation. A formal proof checker gives an unambiguous, mechanical pass-or-fail on every line — a much easier signal to work against than most real-world engineering or writing tasks offer.

The transferable idea isn't that AI can do advanced mathematics — it's that a multi-agent setup paired with a strict, mechanical verifier can work through a problem that would take a specialist years, provided the domain has that kind of unambiguous check available. It's worth remembering the next time a team is scoping something with genuinely high correctness requirements: tests with formal guarantees or automated proof-style verification, rather than code review alone, might be the more relevant lesson here than the headline theorem.

References