Around 1637, Pierre de Fermat claimed a theorem about integer solutions to aⁿ + bⁿ = cⁿ for n > 2. Andrew Wiles produced the first correct proof in 1995. Formalizing that proof — converting it into a form computers can check automatically — has been a long-standing goal. Recently, Anthropic researchers tested whether Claude could make progress on this formalization using the Lean proof assistant. Working largely autonomously over 11 days, Claude produced the first end-to-end, computer-checked proof of Fermat’s Last Theorem. It wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

The proof follows a simplified version of Wiles’s proof from Darmon, Diamond, and Taylor. Human input was limited to occasional high-level instructions. Early attempts failed because agents lost track of the project state and stopped collaborating. The effort succeeded when switching to Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators. Prove2Me maintained a directed acyclic graph of theorem statements, separated theorem statements from proofs to speed compilation, and enabled search and reuse via natural-language descriptions of each theorem.

Using Prove2Me and a Claude Code-based multi-agent harness, a team of agents completed the proof in under two weeks, consuming about six billion output tokens from a general-purpose internal research model. The finished proof was checked by Lean using just Lean‘s three standard axioms. A comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT.

Kevin Buzzard reviewed the proof and noted that this autoformalization achievement demonstrates that AI autoformalization artefacts are now robust enough to be built upon. The ability to automatically formalize large mathematical proofs could catch errors in the common body of mathematical knowledge and reduce the burden of refereeing new work. Anthropic expects it will become common to produce a formalized proof alongside any write-up intended for a human reader, though a formalized proof should not replace human-understandable exposition.

Writing Lean also appears to help Claude prove novel results: it uses partial proofs to independently check hypotheses, much like it writes numerical simulations to check its reasoning. Formalizing FLT was token-intensive, but a small experiment using three personal Claude Max plans formalized Vinogradov’s Three Primes Theorem in three days via Prove2Me. The authors believe collaborative formalization of major results with consumer AI subscriptions is achievable.

Boundaries: Claude‘s proof is over 5x the size of Mathlib, partly because Mathlib is concise and well-reviewed while this proof is likely much longer than necessary. The formalization used a simplified version of Wiles’s proof, not the full 1995 argument. Human involvement was not zero — occasional high-level instructions were given. The result is a verification of an existing proof, not a new mathematical discovery.