Anthropic Says Claude Formalized Fermat's Last Theorem in Lean, Producing 13 Million Lines of Verified Code

Anthropic says its AI model Claude spent 11 days, working mostly autonomously, to produce a complete formal verification of Fermat's Last Theorem using Lean, a computer program that checks mathematical proofs for logical errors. Anthropic announced the result on X, saying the project generated more than 13 million lines of Lean code and proved over 29,500 supporting theorems along the way, many in areas of math that had never been formalized before.

Anthropic called it the largest Lean proof ever written and posted the full code to GitHub, along with a writeup on its Science Blog. According to Anthropic's post on X, the company said experts had expected a project like this to take years, not days.

Fermat's Last Theorem was proven by Sir Andrew Wiles in 1995, more than 350 years after Pierre de Fermat first stated it, closing one of the most famous open problems in mathematics. Claude did not solve a new problem. It took Wiles' existing proof and translated the mathematical reasoning into Lean's formal language, so a machine can verify every logical step holds up.

Coverage hasn't always been careful about this distinction. Bloomingbit's writeup, relaying a Cointelegraph report from September 4, said Anthropic's model "produced a complete proof of Fermat's Last Theorem" and had it "verified by computer." On its own, that phrasing could leave readers thinking Claude proved the theorem itself. It didn't. Anthropic's own account, posted on X, is more precise: Claude performed the formalization of an already-existing proof, and the achievement is the scale and speed of that conversion, not a new mathematical result.

daily.dev's summary gets closer to the real headline, describing the work as a "Lean 4 formalization" spanning 13 million lines of code, and noting it required proving more than 29,000 supporting theorems across math that had never been formalized before.

Checking a major proof by hand can take mathematicians years, because reviewers have to trace every logical step across hundreds of pages of dense reasoning. Formalization tools like Lean force that reasoning into a form a computer can check automatically, catching gaps or errors that human reviewers might miss or take years to find.

Anthropic said in its X post that it sees the project as part of a longer effort to firm up the core of mathematical knowledge, building on three centuries of work by mathematicians and "hundreds of contributors" to Lean and its associated math library, Mathlib. The company argued that AI-assisted verification could reduce the burden on human referees at a time when more mathematical proofs are being produced than ever.

Anthropic's claims here come entirely from its own blog post and GitHub upload, not from an independent mathematical body or a peer-reviewed journal. Lean's automated checker confirms that the logical steps in a formalized proof are internally consistent, but the broader mathematics community still has to independently confirm that the formalization correctly captures what Fermat's Last Theorem and its supporting lemmas actually claim. None of the five sources reviewed here document a response yet from the Lean or Mathlib maintainer communities, or from independent mathematicians, about whether they've reviewed Claude's specific formalization.

The code is public on GitHub, so any mathematician or Lean contributor can inspect it directly. The open question is whether the broader formal-verification community, which maintains Mathlib and reviews contributions to it, validates Anthropic's specific formalization as sound and useful, or flags errors in how the problem was encoded. That review process, not Anthropic's own announcement, will determine whether this becomes a lasting reference work or a footnote in Claude's marketing material.