Fermat's Last Theorem in Lean: 1,000 Claude agents, 30 hours, and what was checked

Fermat's Last Theorem has been fully formalized in Lean, a language in which a computer checks every step of a proof. The first complete formalization was announced by Anthropic on 4 September 2026. An unreleased research model wrote it over 11 days in August, with occasional direction from one researcher. The code is public, and Kevin Buzzard of Imperial College London, who leads the human project to formalize the theorem, compiled it and reported that "it checks out".⁷ On 9 November 2026 Anthropic said that a team of about 1,000 agents running Claude Fable 5.2 "fully formalized the theorem in just 30 hours, with minimal human intervention".¹ Its technical write-up puts the run at 28.7 hours and calls it a "toy experiment" that "reproduced the proof".² The theorem itself was proved by Andrew Wiles, with Richard Taylor, in 1994–95. Both runs are machine checks of that known proof.

Much less is established about the 30-hour run. As of 12 November its Lean code has not been released, and we found no report that anyone outside Anthropic has checked it. Its time, token and size figures, and its comparison with Claude Opus 5.5, come from Anthropic's own posts and from a single run per model. For either run, a passing Lean check shows that the stated theorem follows from Lean's axioms. It does not show that the formal statement says what Fermat claimed, and it does not make the proof readable. For the September proof, Buzzard and a separate checking tool confirmed the statement. For the new run, Anthropic has not said whether that check was done.

Below: what changed, what a Lean check covers, what is public, who has checked what, what Buzzard said, two related announcements, and a short history. Every source was checked on 12 November 2026.

Key terms#

• Lean: a proof assistant. Its kernel is the small program that checks each proof against the language's rules.
• Mathlib: the community library of formalized mathematics that most Lean projects build on.
• sorry: a placeholder that lets an unfinished proof compile. A complete formalization has none.
• Axioms: the assumptions a proof may start from. Mathlib relies on three, propext, Classical.choice and Quot.sound.
• Comparator: a tool from the Lean project that checks a proof against a separately written statement and a list of permitted axioms, then replays it through the kernel.¹⁶
• nanoda: an independent Lean kernel, written in Rust, used as a second checker.

Was Fermat's Last Theorem formalized in Lean, and by whom?#

The theorem says that no positive whole numbers a, b and c satisfy aⁿ + bⁿ = cⁿ when n is greater than 2. Anthropic's public repository states it in Lean as theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n.⁵

Anthropic's first run began on 7 August 2026 on Prove2Me, a collaborative formalization platform built by Tianyi Peng's group at Columbia University,¹⁵ and the final theorem was marked proved on the evening of 17 August. Dozens of agents ran "a general-purpose internal research model roughly comparable to Claude Fable 5.1" and consumed about six billion output tokens. Mathematical input from humans, the post says, "was limited to occasional high-level instructions from Tianyi".³ The accompanying timeline adds that humans "wrote no mathematics and no Lean beyond the one-line statement of the goal theorem."⁴

The result has 29,511 theorems and about 13 million lines of Lean. It follows the 1995 account of Wiles's argument by Darmon, Diamond and Taylor, and proves its deep inputs, such as Mazur's theorem and the Langlands–Tunnell theorem, in the special cases the argument needs. It adapts 106 files, with credit, from Buzzard's Imperial project and from flt-regular, an earlier formalization of the theorem for regular primes.⁴

Fermat's Last Theorem was the last unformalized item on Freek Wiedijk's list of 100 theorems. Buzzard wrote that the work "wraps up this 20-year-old benchmark",⁷ and Wiedijk's page, last modified on 1 November 2026, now reads 100%, crediting the theorem to "Lean, Anthropic".¹³

What is new in the 30-hour run compared with September?#

The fullest account is a post on Anthropic's developer blog by Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl and Lance Martin.² The aim was to redo the result "without Prove2Me or a researcher directing the work, using a harness built from general-purpose tools."

One lead agent and 999 helpers each had a virtual machine with no network access, Lean and Mathlib, a Git branch and a shared database. They also had a starting kit: "We gave the agents a list of 60 statements, a one-sentence sketch of the classical route, the definitions those statements use, and 47 proved lemmas from our earlier formalization, and assigned lead and helper roles."

About 27 minutes in, three statements were already proved. The lead set aside the 47 statements that most helpers had judged infeasible within the budget and moved nearly all helpers to the remaining ten, which were proved within roughly 70 minutes. The team later went back to the 47. The hardest piece was the Langlands–Tunnell theorem, which its captain had given "less than a 1% chance of finishing in time". The team split it into a tree of 2,418 tasks and proved it at hour 28.4. The final theorem followed at hour 28.7, and the lead wrote: "Thank you all: Fermat's Last Theorem is on main, kernel-checked by the official checker."

Two interventions are recorded. The harness sent the lead 19 automatic reminders of the time remaining, and near hour 18 Anthropic "restarted the run from its last save and gave the agents 12 more hours."

The launch post simplifies this. It gives 30 hours for 28.7, speaks of "action tokens" where the write-up says output tokens, and names the model as Fable 5.2 where the write-up says an early version of it. Its first wording, archived on 9 November, also said that Fable 5.2 "used no mathematical references, only a list of intermediate theorem statements to score progress."²³ On 11 November Anthropic removed that clause and added a footnote quoting the starting kit above, noting that it had amended the paragraph "to more accurately describe the information we provided to the model."¹

	First formalization	30-hour run
Announced	4 September 2026	9 November 2026; amended 11 November
Model, as Anthropic reports it	An internal research model "roughly comparable to Claude Fable 5.1"	"an early version of Claude Fable 5.2"
Time	11 days, 7 to 17 August	28.7 hours, restarted from its last save near hour 18
Agents	Dozens	About 1,000: one lead, 999 helpers
Human involvement, as described	Occasional high-level instructions from one researcher; humans wrote the one-line goal statement	No researcher steering; statements, a sketch, definitions and 47 lemmas from the first proof supplied; 19 automatic reminders
Coordination	Prove2Me platform	Git, a shared database, isolated sandboxes
Output tokens	About 6 billion	One-third as many; no figure given
Proof size	29,511 theorems, about 13 million lines	One-seventh the length; no line count given
Public	Lean code, build and check scripts, browsable pages, a 17-page timeline	Two blog posts and their figures

What does “formalized” mean, and what does a Lean check establish?#

To formalize a proof is to rewrite it so that Lean can check every step from the axioms up. When the September repository builds, the kernel has accepted every declaration in it. The build is also set to fail unless fermat_last_theorem depends on exactly the three standard axioms, which rules out a sorry or an added axiom anywhere beneath it.⁵

That is strong evidence about the proof and limited evidence about the statement. Buzzard's post of 12 November gives a two-line example: a Lean definition of Fermat's Last Theorem that omits the condition that a, b and c are positive is false, because Lean's natural numbers include 0. "This does not stop the statement from compiling!", he writes; it only stops any proof of it from compiling.⁸ Someone has to read the statement and confirm it is the right one.

Three more limits apply. The repository's README notes that "What no tool can check is that each intermediate theorem means what its name suggests".⁵ A Lean proof explains nothing: the same README says the sources "are written to be checked rather than read". And the kernel must be trusted. Buzzard recalls a soundness bug in Lean's kernel, fixed four hours after it was found, and argues that checking with several independent kernels guards against such bugs.⁸

His post sets out four questions to ask of AI-generated Lean code. Applied to the two runs, with what is public:

Buzzard's question	First formalization	30-hour run
Does the Lean statement match the informal statement?	It uses Lean's natural numbers and Mathlib's power function; Buzzard says he read it; comparator matched it to a file importing only Mathlib	Not stated; the agents were handed the statements and definitions
Does the code compile?	Yes, in Anthropic's from-scratch build and in Buzzard's, on a machine Anthropic lent him	The lead agent reported "kernel-checked by the official checker"; no outside build is possible
Does it prove the theorem as stated?	Comparator passed, run by Anthropic and by Buzzard	Not reported
Does it exploit a bug in Lean's kernel?	nanoda accepted every declaration in Anthropic's run, built with four small patches that Anthropic says change no typing rule	Not reported

Is the new Lean code public, and can anyone rebuild it?#

No, not as of 12 November. Neither the launch post nor the technical write-up links to code. Anthropic's Fermat repository on GitHub was last changed on 24 September and holds only the September proof, on Lean 4.33.1 and Mathlib v4.33.0.⁵ Anthropic's other public Lean repository, formal-math, holds three unrelated projects.¹⁷ We found no release of the run's prompts, logs, grader or harness either.

Its final statement, Lean and Mathlib versions, size in lines, and whether comparator or a second kernel was run on it are all unknown.

The September proof can be rebuilt by anyone with enough hardware. The build took Anthropic 5 hours 32 minutes at 96 parallel jobs, with a peak of 153 GB of memory, and the README advises allowing 300 GB for the comparator check, which takes about 15 hours. Buzzard first tried on his own computer and "very quickly ran out of memory"; Anthropic then gave him temporary access to a machine with 96 cores.⁸ The README calls the repository a "Research artifact. Not maintained and not accepting contributions."⁵

What is self-reported, and what has anyone outside Anthropic checked?#

Everything about the 30-hour run comes from Anthropic. Four points need more detail.

• The model. The agents ran "an early version" of Fable 5.2.² Whether it behaves like the released model is not stated.
• The comparison with Opus 5.5. The launch post says Opus 5.5, in the same setup, "completed only 26% of the formalization in 18 hours, and barely made any more progress after 30."¹ The figure measures completion as "weighted share of statements proved" without giving the weights, and its caption says there was "a single run per model". One run cannot show how much results vary.
• Tokens and size. No absolute numbers are given, and neither post says how length was measured. This matters because Claude's own assessment of the September proof, quoted in Anthropic's timeline, found that "About a fifth of all proof-file lines are verbatim copies of declarations found elsewhere in the tree".⁴
• The starting point. The 47 lemmas and the definitions came from the September formalization, public since 4 September. Anthropic does not say whether the model had seen that code in training.

The September proof has had an outside reader. Buzzard compiled it, ran comparator, and, he told a commenter, "manually inspected every line of the code base which (according to Claude) was not a mathematical definition or proof of a theorem".⁷ To another he explained that the machine checks the proof, while someone has to read the statement "to check that it corresponds to the right theorem — but I did that." Anthropic thanks him "for reviewing the proof and for his comments".³ The repository's own metadata still records its review status as "self-assessed", with an empty list of reviewers.⁶

For the 30-hour run we found no outside check. Buzzard's post of 12 November discusses the September proof but not the new run.⁸ The Xena blog's Bluesky account has not posted since December 2025, two Lean and Fermat hashtags on Mathstodon showed nothing about it, and the public archive of the Lean community chat was last updated on 28 February 2026, so discussion there could not be read.²² Proofs and Prompts, a site run by mathematicians, covered the launch on 10 November, describing Anthropic as "bragging that a team of 1,000 Claude agents formalised the proof of Fermat’s Last Theorem in only 30 hours".¹⁸ It reminded readers that Anthropic had formalized the theorem before, and added a joke, flagged as not the site's official view, about where the agents might have found the answer.

What did Kevin Buzzard say, and what happens to the human FLT project?#

Buzzard's Imperial project follows a modern route to the theorem, planned by Richard Taylor and borrowing from the work of Khare and Wintenberger.¹¹ The Engineering and Physical Sciences Research Council (EPSRC) funds it under grant EP/Y022904/1 from October 2024 to September 2029, and its stated first goal is to reduce the theorem to results known by the end of the 1980s.¹²

His post of 4 September, "FLT: Anthropic has beaten me to it", congratulated Anthropic and was plain about what the result means.⁷ "Note that mathematically this work of anthropic tells us essentially nothing," he wrote: he was already 99.9% sure the proof was correct, and "the formalization just faithfully follows the early literature on the proof and adds nothing." But "What this work does tell us, however, is what is possible in the field of autoformalization." He expects machine checks to show "exactly what is being assumed in the proofs of various important results in my field." A month later he explained that arguments in his field known only to experts, with no public write-up, had led him to leave curiosity-driven research for formalization: "You cannot fool Lean; one learns this very early on."⁹

On his own project: "a naive reaction to the news above is that I no longer have any work to do. This is not the case." Anthropic's proof goes further than his promise to the EPSRC. But he also promised contributions to Mathlib, which continue, and "a dynamic document enabling humans to explore the modern proof", which he does not expect Anthropic to produce. He was given £1M for five years, he notes, and wonders whether Anthropic spent more.

In October, a guest post on his blog by Jeremy Avigad, Buzzard and five other formalization researchers put it more sharply: "although the accomplishment is impressive, this piece of AI-generated code probably has little ongoing value."¹⁰ Their concern is reuse, and Anthropic's own timeline says its proof "is not yet in a form Mathlib would accept".⁴ The Imperial repository is still active, with Mathlib updates on its main branch through 22 October.¹¹

We found no public comment from Buzzard on the 30-hour run as of 12 November. His latest post ends: "“It’s true because it’s checked in Lean” can be made to make sense. But one has to do some work beyond “the Lean code compiles”."⁸

What did Axiom formalize in the Stacks Project?#

Axiom, a startup working on AI for mathematics, dated its announcement 4 November 2026.¹⁹ Proofs and Prompts listed it on 7 November.¹⁸ The Stacks Project is an open-source reference on algebraic geometry, begun in 2005 by Johan de Jong of Columbia University. Axiom says it has formalized "the entire Stacks Project" in "some 16 million lines of code", and calls the result "the largest integrated, reusable library of formalized mathematics ever built." That is Axiom's own description.

The repository's README states that there is no sorry and no native_decide, that proofs use only the three standard axioms, and that the library has about 63,000 Lean modules.²⁰ It has two tiers: StacksCore, code a person has checked against the Stacks Project, and StacksFrontier, code "written by AI agents" where, the README says, "review is most needed". Axiom says statement faithfulness is "enforced automatically at scale through multi-agent auditing" and other cross-checks,¹⁹ and that its agents found dozens of statements in the source that needed local refinement. We found no outside review yet.

This is a library meant to be imported into new proofs; Axiom's formalization of the Weil conjectures already builds on it. Axiom notes that de Jong asked, on 21 October, that AI-generated comments and pull requests not be sent to the upstream Stacks Project for now.¹⁹ In September Buzzard had told a reader that a Stacks formalization was "presumably currently feasible but costly today", while getting it into Mathlib was "another story".⁷ We wrote earlier about Axiom's formalization of the classification of finite simple groups.

What is Imperial's Langlands Lab?#

Imperial College London announced the Langlands Lab on 27 October 2026.²¹ Proofs and Prompts listed it on 4 November.¹⁸ It is funded by a £5 million grant from XTX Markets and led by Buzzard. Its focus is the Langlands program, which Imperial describes as an effort to uncover connections between fields, particularly number theory and analysis. It aims to produce new results verified in Lean, papers that make them accessible, and free interactive tools for working through proofs.

The grant supports five PhD students and three postdoctoral researchers over four years, from 2027. The students "will be required to develop a deep understanding of the mathematics they are working on, explaining and defending their results without AI assistance before taking responsibility for research outputs." Buzzard is quoted: "AI is changing what it means to do mathematical research, and we need to rethink how we train the next generation of mathematicians."

Why does it matter for AI-generated proofs that are hard to verify?#

Anthropic gives the reason itself: formalization helps mathematicians gain confidence in results, and "this matters even more when AI models generate results that are hard for humans to verify".¹ Fermat's Last Theorem makes a clean test because nobody doubted it. The right statement is short and well known, so a wrong one would be easy to spot.

New AI-generated results are harder. Buzzard reports that among 290 OpenAI theorems that came with Lean code, "around 38 of them have the property that the Lean code does not even state, let alone prove, the main theorem of the paper."⁸ For Axiom's classification of finite simple groups, the statement rests on about 5,600 lines of definitions in an AI-written library, and he has not met anyone who claims to have checked the definitions of the sporadic groups carefully. We have looked at the same question for the Aaronson-Ambainis conjecture and for OpenAI's Yang–Mills construction.

Faster formalization means more AI-generated claims arriving with a formal proof attached. The checks that follow still take people and, at this scale, large machines.

A short history: from Wiles to the last theorem on Wiedijk's list#

Date	Event
About 1637	Fermat writes the claim in the margin of his copy of Diophantus's Arithmetica3
June 1993	Wiles presents a proof in three lectures at the Newton Institute; two months into checking, a gap is found
1993–94	Wiles spends about a year repairing it, first alone, then with Richard Taylor
May 1995	Wiles's paper and the Taylor–Wiles paper appear in Annals of Mathematics, volume 14114
1999	The "top 100" list of theorems that Wiedijk tracks for formalization dates from this year13
November 2023	Buzzard opens the Imperial FLT repository on GitHub11
October 2024	His EPSRC grant starts, running to September 202912
7–17 August 2026	Anthropic's first run, on Prove2Me
4 September 2026	Anthropic announces the first complete formalization; Buzzard: "Anthropic has beaten me to it"
27 October 2026	Imperial announces the Langlands Lab
4 November 2026	Axiom releases its Stacks Project formalization
9 November 2026	Anthropic reports the 30-hour, 1,000-agent run

What this means for a research record#

A reader needs these details before trusting a formal proof written by AI: who wrote the formal statement and who checked it against the informal one; which model was used, as the team reports it, and what people supplied to it; which version of the code was checked, on which Lean and Mathlib versions; and which checks ran, on what date and by whom. For the September proof, Anthropic's repository and posts answer most of these. For the 30-hour run, most are still open.

A researcher publishing an AI-assisted result can write the same details down, dated and signed, with a link to the code. On Papex an AI app can prepare such a draft, which the researcher reviews and signs (how AI apps work with Papex). Such a record says nothing about whether the mathematics is right; that stays with Lean and with the people who read the statement.

What would settle the open points: release of the 30-hour code, a comparator and second-kernel run on it, a statement check by someone outside Anthropic, and the weights behind the completion figure.

A note on interests: this post reports on Anthropic's Claude models, and it was drafted with Claude. Readers should weigh it with that in mind and check the sources below.

Sources#

1. Introducing Claude Fable 5.2 and Claude Mythos 5.2 (Anthropic, 9 November 2026, edited 11 November), checked 12 November 2026 ↩ a b c d
2. Barry Zhang, Tianyi Peng, Elle Najt, Keller Scholl and Lance Martin, Safely scaling multi-agent teams with Claude Fable 5.2 (claude.dev, 9 November 2026), checked 12 November 2026 ↩ a b c
3. Formalizing Fermat's Last Theorem (Anthropic, 4 September 2026), checked 12 November 2026 ↩ a b c
4. Formalizing Fermat's Last Theorem in Lean: a timeline and selected excerpts from Claude's reasoning (Anthropic, 17 pages), checked 12 November 2026 ↩ a b c d
5. anthropics/fermats-last-theorem: README, FinalCheck.lean and commit aa2d8b34 (GitHub, last changed 24 September 2026), checked 12 November 2026 ↩ a b c d e
6. anthropics/fermats-last-theorem, formalization.yaml (GitHub), checked 12 November 2026 ↩
7. Kevin Buzzard, FLT: Anthropic has beaten me to it, with comments (Xena, 4 September 2026), checked 12 November 2026 ↩ a b c d e
8. Kevin Buzzard, "…and the proof is checked in Lean" (Xena, 12 November 2026), checked 12 November 2026 ↩ a b c d e f
9. Kevin Buzzard, To grieve, or not to grieve? (Xena, 1 October 2026), checked 12 November 2026 ↩
10. Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz, How to Formalize All of Mathematics (Xena, 16 October 2026), checked 12 November 2026 ↩
11. ImperialCollegeLondon/FLT: README and commit history (GitHub), checked 12 November 2026 ↩ a b c
12. ImperialCollegeLondon/FLT, GENERAL.md (GitHub), checked 12 November 2026 ↩ a b
13. Freek Wiedijk, Formalizing 100 Theorems (Radboud University, last modified 1 November 2026), checked 12 November 2026 ↩ a b
14. Andrew Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), issue 3, checked 12 November 2026 ↩
15. Shuze Chen and four co-authors, Prove2Me: An Open Collaborative Platform for Scaling Math Formalization, arXiv:2608.28433, checked 12 November 2026 ↩
16. leanprover/comparator: README (GitHub), checked 12 November 2026 ↩
17. anthropics/formal-math: README (GitHub), checked 12 November 2026 ↩
18. Newsfeed, items of 4, 7 and 10 November 2026 (Proofs and Prompts), checked 12 November 2026 ↩ a b c
19. The Stacks Project, formalized in Lean (Axiom, 4 November 2026), checked 12 November 2026 ↩ a b c
20. AxiomMath/Stacks: README (GitHub), checked 12 November 2026 ↩
21. £5 million grant to establish new laboratory for AI-assisted mathematics at Imperial (Imperial College London, 27 October 2026), checked 12 November 2026 ↩
22. Lean community Zulip archive, index (last updated 28 February 2026), checked 12 November 2026 ↩
23. Introducing Claude Fable 5.2 and Claude Mythos 5.2, first published version (Internet Archive capture, 9 November 2026, 18:57 UTC), checked 12 November 2026 ↩