Formalisation of Fermat’s Last Theorem – Astonishing Throughput
We live in interesting times – Anthropic agents have produced a machine-checked proof of Fermat’s Last Theorem1. Note, AI didn’t solve FLT – no new mathematics – Wiles and Taylor did that in the 90s. What the agents did was formalise a proof so that a machine verifies every single step, and they did it in 11 days.
Some detail on what that means, because a lot of the coverage has been muddled.
Fermat scribbled the claim in a margin around 1637. Wiles announced a proof at the Newton Institute in 1993, a reviewer found a gap in it a few months later, and Wiles patched it with his former student Richard Taylor, publishing in 1995.
Formalising a proof is a different job from finding one. It means rewriting the argument in a language, in this case Lean2, where a computer checks every inference against a small set of axioms. Human proofs skip whatever a competent reader would fill in for themselves. Lean fills in nothing.
The route the agents took is the Darmon-Diamond-Taylor exposition of the Wiles-Taylor-Wiles argument, via the Langlands-Tunnell theorem and Ribet’s level lowering. This is different to the route Kevin Buzzard has been formalising at Imperial College London. His EPSRC-funded project follows the more modern proof and has other deliverables besides, including pushing fundamental objects from modern number theory into Mathlib and building a document that lets humans explore the argument. Anthropic’s repository borrows pieces from his project and from flt-regular.
The scale of the run: dozens of agents working in parallel, coordinated through a dependency graph on a platform called Prove2Me. Roughly six billion output tokens. Thirteen million lines of Lean, 30,300 theorems proved and 29,500 used in the final proof. Buzzard measured the repository at 13.4 million lines and reports that it takes nearly twenty times as long to compile as the whole of Lean’s mathematics library, on a 96 core machine.3
Kevin Buzzard also checked the output: he compiled the code himself and ran comparator, the standard tool for confirming that the theorem proved actually matches Mathlib’s own statement of FLT. Then he went looking for the obvious cheat. Lean has had soundness bugs found in it recently, and an agent that stumbled on one could in principle use it to prove anything at all, including false things. Buzzard had an agent flag every line in the repository that was not a mathematical definition or a proof, and inspected by hand the hundred or so lines that came back. He notes as well that OpenAI’s models have been over Lean’s codebase and found no soundness issues in the version used here.
Interesting takeaway: Anthropic’s post says proof assistants demonstrate correctness beyond a doubt, which is too strong, and a commenter on Buzzard’s blog said as much. Trust did not become mechanical here. It moved, from checking the mathematics to checking that nobody had gamed the checker. Smaller job, still a human one.
Should we trust the result? There were a hundred or so lines that were considered suspicious which turned out to define a convenience tactic. Nobody had gamed the checker.
Why the throughput matters
The throughput is astonishing. A job the field expected to take years was done in 11 days. Commenters have guessed the token cost at somewhere between $100,000 and $300,000, against a five year, £1M grant for the human project, though nobody outside Anthropic knows the real figure and the comparison to Buzzard’s work is unfair since he promised his funder several things that the Anthropic work does not deliver. Still, the order of magnitude is incredible.
If thousands of pages of research mathematics can be autoformalised4 at this rate, refereeing gets faster and errors sitting in the published literature become findable. Papers that quietly lean on results only known to the experts get flagged for what they are actually assuming, which is Buzzard’s reason for excitement, since he wants machines auditing parts of the Langlands programme that have had far less scrutiny than FLT ever did. And AI-generated mathematics, now arriving faster than humans can check it, becomes checkable at something near the rate it is produced – which one could say is a kind of scalable oversight.5
This also checks off the last open item on Freek Wiedijk’s list of 100 formalisation challenges, a benchmark that has stood for twenty years. The successor list runs to over a thousand theorems and most of it is still open.
Proofs are still hard, verifying them just got easier
The reason any of this worked is an asymmetry. Finding a proof is hard, checking one is cheap and mechanical, so you can throw an enormous number of candidate steps at a kernel6 that answers near instantly and cannot be argued with. Three conditions make that possible: a fixed formal language with agreed axioms, a verifier small enough that a human can read it, and an independently written statement of the target to compare your result against.
That combination is rare outside of mathematics and software verification. So if we extrapolate from this result to AI solving hard problems generally, the question we should be asking is “what plays the role of the kernel?” In the empirical sciences it is experiment, which is slow and expensive. In ethics there is nothing that fits the role at all, which is a good part of why alignment is hard rather than merely laborious.
Idea generation has scaled. Verification is the thing that usually doesn’t, and this result is impressive because the verification of proofs is one of the uncommon cases where verification scales too.
See Anthropic’s post here: https://www.anthropic.com/research/formalizing-fermats-last-theorem
And Kevin Buzzard’s write-up here: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
Footnotes
- Fermat’s Last theorem states that no three positive integers a, b, and c can satisfy the equation \(a^n + b^n = c^n\) for any whole number n greater than 2. ↩︎
- Lean is a modern functional programming language and proof assistant that is increasingly being used by mathematicians to digitise and verify complex modern mathematics. Lean was created at Microsoft Research by Leonardo de Moura, but development moved to the Lean FRO, a non-profit set up in 2023, and de Moura is now at AWS. ↩︎
- The thirteen million lines measure how verbosely this particular swarm writes Lean, not how deep the theorem is. Anthropic concede in a footnote that the proof is likely far longer than it needs to be, and Mathlib holds a large slab of undergraduate and graduate mathematics in about a fifth of the space. ↩︎
- Autoformalisation is the process of using artificial intelligence to automatically translate human-written mathematical text or informal proofs into a rigorous, machine-readable language (like Lean). ↩︎
- Scalable oversight is the challenge of providing reliable supervision and training signals for artificial intelligence systems as they become smarter and more complex than their human creators. ↩︎
- In formal mathematics, “the kernel” (or logical kernel) refers to the small, foundational core of a proof assistant that is solely responsible for verifying the mathematical validity of a proof. Acting as the final gatekeeper, it shifts the burden of trust from massive, complex codebases or lengthy human proofs to a compact, independently verifiable checker. ↩︎
