AI continues to make rapid advances in science and math.
Anthropic says its AI model Claude has produced the first complete, computer-verified proof of Fermat’s Last Theorem, one of the most famous problems in the history of mathematics. The company says Claude worked largely on its own for 11 days to turn a legendary 129-page human proof into a form that a machine could check line by line, with zero room for error.
What Is Fermat’s Last Theorem, And Why Does It Matter
Back in 1637, French mathematician Pierre de Fermat scribbled a claim in the margin of a book: there are no positive whole numbers a, b, and c that can make the equation aⁿ + bⁿ = cⁿ true, for any power n greater than 2. He added a now-famous line saying he had a “truly marvelous proof” of this, but that the margin was too small to contain it.
That proof, if it ever existed, was never found. For over 350 years, the world’s best mathematicians tried and failed to crack it. In 1908, a huge cash prize (worth roughly $1-2 million today) was offered for a correct proof, and more than 600 wrong attempts poured in during the very first year.
It wasn’t until 1995 that British mathematician Andrew Wiles finally cracked it, using advanced mathematical machinery that didn’t even exist in Fermat’s time. Wiles’s proof ran 129 pages, and even that had a critical error discovered mid-review that took him and a collaborator over a year to fix. Verifying it properly took the mathematical community months of painstaking, expert-level checking.
What Anthropic Actually Did
Checking a proof by hand is slow and can still miss mistakes, even when experts pore over it for months. So mathematicians have increasingly turned to “proof assistants,” software like Lean that can verify mathematical logic automatically, the same way a calculator verifies arithmetic. The catch is that translating a human proof into a language a computer can fully understand and check, a process called “formalization,” is brutally tedious. A human proof skips over steps that are “obvious,” but Lean needs every single step spelled out, and it can only build on the small fraction of mathematics that has already been formalized before it.
For this reason, formalizing Wiles’s proof of FLT was expected to take the mathematical community years. A team led by Kevin Buzzard at Imperial College London kicked off exactly that kind of multi-year, human-led effort back in 2024.
Anthropic says Claude did it in 11 days. Working through a system called Prove2Me, an open collaborative platform built by Anthropic researcher Tianyi Peng and his team at Columbia University, dozens of Claude agents worked in parallel to break the proof down into smaller pieces, prove each one, and stitch them back together. In the process, Claude wrote 13 million lines of Lean code and proved roughly 30,300 individual smaller theorems along the way, more than five times the size of Mathlib, the main community library of formalized mathematics that the proof relies on. Human involvement was reportedly limited to occasional high-level nudges, like suggesting which sub-problem to prioritize next.
Kevin Buzzard, whose team had been working on this exact formalization, reviewed Claude’s output and called it an extraordinary achievement, noting that the proof rests on nothing but the basic axioms of mathematics and touches on formalized algebra, geometry, harmonic analysis, and number theory all at once.
Not every attempt went smoothly. Anthropic says some of Claude’s early efforts lost track of the project’s state and agents stopped coordinating effectively, though those failed attempts still ended up contributing a small slice of the final proof’s code.
Why This Matters Beyond One Famous Equation
The headline is Fermat’s Last Theorem, but the more important story might be what this says about verifying AI-generated science in general. AI systems are now producing mathematical claims faster than human reviewers can check them. Formalization offers a way to let a computer do the checking instead of asking an overworked human referee to trust their gut.
This isn’t happening in isolation. AI labs and startups have been racing to attach machine-checked proofs to big mathematical claims over the past year. Fields Medalist Terrence Tao has warned that this comes with real hazards, pointing out that AI-generated proofs can look flawless on the surface while hiding subtle errors that a human mathematician would never make, which is exactly the kind of risk that formal verification tools like Lean are designed to catch. The volume of AI-assisted math claims has grown large enough that trackers now exist just to keep score, with one recent count showing OpenAI credited with 234 solved math problems and Anthropic with 57. Competing labs have also been formalizing famous unsolved problems in Lean, including an effort by the startup Axiom Math that produced the closest machine-checked result yet to the twin prime conjecture. Elsewhere, a math-focused startup founded by Robinhood CEO Vlad Tenev made news after its AI system was said to have cracked an Erdős problem that had been open for three decades, formalized in Lean from the outset.
Anthropic argues that pairing every new AI-generated proof with a formal, Lean-checked version could become standard practice going forward, not to replace the human-readable write-up mathematicians rely on to actually understand a result, but to give reviewers a fast, mechanical way to confirm it isn’t wrong. The company also points to a smaller demonstration of the same idea: three researchers using ordinary consumer Claude subscriptions formalized a proof of Vinogradov’s Three Primes Theorem in just three days, suggesting this kind of large-scale formal verification may not require a research lab’s worth of compute.
The full proof and a written walkthrough have been published on GitHub for anyone who wants to check Claude’s work for themselves.