Fermat’s Last Theorem, in Lean?

The claim, in plain words

Episode AN01 covers a release by Anthropic on September 4, 2026: a blog post, a public Lean repository with a written walk-through of the proof’s route, and a companion document with excerpts of Claude’s reasoning. Anthropic calls it the first complete computer-checked proof of Fermat’s Last Theorem. In Anthropic’s account, a team of Claude agents worked largely autonomously for 11 days, from August 7 to August 17. The proof has 29,511 theorems and about 13 million lines of Lean, about 10.5 million without generated boilerplate; our estimate from a sample of 440 files is 13 to 15 million. Anthropic calls it the largest Lean proof ever constructed, and adds in a footnote that it is likely much longer than it needs to be. The post says the run used about 6 billion output tokens from an internal research model, that the proof uses just Lean’s three standard axioms, and that a comparator confirmed its statement matches Mathlib’s own statement of the theorem.

Who did what. Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, set up the test. The post says human mathematical input was limited to occasional high-level instructions from him, such as: Jacobian as a scheme sounds high priority. The companion document says humans wrote no mathematics and no Lean beyond the one-line statement of the goal theorem. The agents worked through Prove2Me, a platform from Peng’s group that keeps a shared graph of theorem statements for agents to claim. The proof builds on Lean’s community library, Mathlib, and adapts pieces from two human projects, credited file by file: Buzzard’s Imperial project and flt-regular. The companion document says the opening reduction follows the Imperial project’s blueprint, and the repository’s notice counts 106 files with material from the two.

What it doesn’t claim

What is not claimed. This is not new mathematics: the post says that what is new is the verification. Buzzard writes that, mathematically, the work tells us essentially nothing, since the proof was already accepted and the formalization follows the early literature; what it does show, he writes, is what is now possible in autoformalization. It is not the modern proof that Buzzard’s project is formalizing. The named deep theorems are proved only in the special cases the argument needs; the walk-through says, for example, that Ribet’s theorem is not proved for a general representation. And the companion document says the code is not yet in a form Mathlib would accept.

Where it stands

Announced; code public

Anthropic’s post and the repository, September 4, 2026 (first commit dated September 3; the Lean files have not changed since)

Outside check: Kevin Buzzard

His blog, September 4: “I’ve compiled the code base and run comparator on it — it checks out.” In comments there (September 5) he adds that he spent many hours looking over the code and inspected the 100 or so lines that are not definitions or proofs (“Obviously this is not a perfect approach”). Anthropic’s post quotes him and thanks him “for reviewing the proof and for his comments”

Peer reviewed

No. The repository’s metadata calls its review “self-assessed”

Lean proof, by Anthropic

The claim itself: Lean’s three standard axioms (propext, Classical.choice, Quot.sound), comparator against Mathlib’s statement, a second kernel (nanoda, with Anthropic’s published speed patches), as the README reports. Not built or run by us

Last checked October 27, 2026. Where it stands. The post and the repository went public on September 4; the repository’s first commit is dated the day before, and its Lean files have not changed since. Outside check: Kevin Buzzard. On his blog that day he wrote: “I’ve compiled the code base and run comparator on it — it checks out”. In comments there, he adds that he spent many hours looking over the code and inspected the hundred or so lines that are not definitions or proofs. Anthropic quotes him calling it an extraordinary autoformalization achievement. The repository’s own metadata calls its review self-assessed, and nothing is peer reviewed. The Lean is the claim itself, by Anthropic; we did not build or run it. Its README says one build took 5.5 hours at 96 jobs, and the comparator about 15 hours more.

The caveats, from the sources themselves. Claude’s own assessment, in the companion document, says roughly two in five theorem statements in the proof files repeat, word for word, a statement made in another file. The README says no tool can check that each intermediate theorem means what its name suggests. And on October 16, a guest post on Buzzard’s blog, by seven mathematicians and formalizers, including Buzzard, said that although the accomplishment is impressive, this code probably has little ongoing value. For comparison, on stated facts only: Axiom’s classification release, in episode AX01, reported 43.1 million lines in 24 days, and both repositories call their review self-assessed. If it holds, Fermat’s Last Theorem, as proved by Wiles and Taylor, has a complete computer check in Lean, long and machine-written, with intermediate statements that, as its README says, no tool can check for meaning.

How the proof goes

1. The question. Here is the history as Anthropic’s post tells it. Around 1637, Fermat wrote the claim in the margin of a book. In June 1993, Andrew Wiles presented a proof in three lectures. A reviewer’s question exposed a gap, which Wiles fixed with his former student Richard Taylor, and the proof was published in May 1995. Darmon, Diamond and Taylor later wrote an exposition, which the post calls a simplified version of Wiles’s proof. Checking such a proof by computer means writing every step in a proof assistant such as Lean. In 2024, Kevin Buzzard at Imperial College London started a multi-year community project to do this. Its own README says it follows a more modern route and is funded until 2029. A separate project, flt-regular, had already formalized the theorem for regular primes.
2. The route. How the proof goes, as the walk-through lays it out. It is a proof by contradiction. Exponents three and four come from Mathlib. Five is settled by a descent; seven, eleven and thirteen by Kummer’s theorem for regular primes, ported from flt-regular. For a prime p from seventeen up, a counterexample gives a Frey curve: y squared equals x, times x minus a to the p, times x plus b to the p. Step one, Mazur: the curve’s mod p representation is irreducible. Step two, Wiles: the curve is modular, through the Langlands–Tunnell theorem at the prime three, a switch between three and five, and modularity lifting, R = T. Step three, Ribet: level lowering takes the representation down to level two. And at level two there are no cusp forms of weight two, which the repository proves from Mathlib. As background, by the standard genus formula, which our script checks, the modular curve of level two has genus zero. That is the contradiction.
3. The run. How the run went, in Anthropic’s account. Early attempts failed: agents lost track of the project’s state and stopped collaborating effectively, and the post says those efforts still make up about 7% of the non-boilerplate lines. On Prove2Me, agents usually checked one another’s statements first, which the companion document says caught several false statements early. On August 17, the final theorem read proved on the platform; one agent added, modulo re-check. The re-check was needed, because the platform checks each statement’s proof separately. The team then built everything as one Lean project, whose build fails unless the final theorem rests on exactly the three standard axioms. The comparator replayed the whole proof through Lean’s kernel, and nanoda, a second, independent kernel, run with small speed patches that Anthropic published, accepted every declaration.

Not in the video: the post also reports a small side experiment in which agents on three personal Claude Max plans formalized Vinogradov’s three primes theorem in three days, collaborating through Prove2Me.

The numbers in the video

• Ours: 52 Pythagorean triples with c ≤ 100; no solutions of aⁿ + bⁿ = cⁿ for n = 3 to 10 with c ≤ 300 (an illustration, not a proof); the near misses 6³ + 8³ = 9³ − 1 and 9³ + 10³ = 12³ + 1.
• Ours: the modular curve X₀(2) has genus 0 by the standard formula, so there are no weight-2 cusp forms of level 2 (the repository proves this from Mathlib by its own route).
• Ours: an estimate of the repository’s Lean line count from a random sample of 440 files: 14.1 million (95% interval 12.9 to 15.3 million). Anthropic says about 13 million; Buzzard’s blog says over 13.4 million.
• From the repository tree: 29,511 statement files, 29,511 proof files and 1,450 definition modules.
• From the sources: 11 days (August 7 to 17, 2026); about six billion output tokens; about 7% of non-boilerplate lines from failed early attempts; 106 files with material from the Imperial FLT project and flt-regular.

Read the source

• Anthropic: “Formalizing Fermat’s Last Theorem” (September 4, 2026).
• The Lean repository (Apache-2.0; not run by us) and its walk-through, PROOF-PATH.md.
• Anthropic’s companion document: a timeline and excerpts of Claude’s reasoning.
• Kevin Buzzard: “FLT: Anthropic has beaten me to it” (September 4, 2026), and the guest post “How to Formalize All of Mathematics” (October 16, 2026).
• The human projects it builds on: the Imperial College London FLT project, led by Kevin Buzzard, and flt-regular; the platform Prove2Me.
• For comparison: episode AX01, on Axiom’s Lean formalization of the classification of finite simple groups.

AI Proved What? is independent and not affiliated with Anthropic beyond using its product Claude.

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.