AI Proved What?

AN04 (outside OpenAI’s math catalogue), November 2026

Fermat’s Last Theorem in Lean in 30 hours?

Anthropic says about 1,000 Fable 5.2 agents redid its September Lean formalization of Fermat’s Last Theorem in about 30 hours. No code from the run is public yet, and no outside check is named.

Disclosure. Anthropic makes Claude, which helps make this series. This is Anthropic’s own claim: we hold it to the same standards as every other lab’s, using only public sources. AI Proved What? is independent and not affiliated with Anthropic beyond using its product Claude.

Play AN04: Fermat in Lean in 30 hours? A grid of 1,000 orange dots for the agents, a long blue bar (11 days) and a short orange bar (30 hours) drawn to scale, and an empty page with a question mark for the code that is not public.

6:22. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:17The claim
  3. 2:45How the run went
  4. 4:36Where it stands

The claim, in plain words

This is AN04. Before we start: Anthropic makes Claude, which helps make this series. This is Anthropic’s own claim: we hold it to the same standards as every other lab’s, using only public sources. Fermat’s Last Theorem says that for any whole number n of at least three, no positive whole numbers a, b and c satisfy aⁿ + bⁿ = cⁿ. Cubes come close: 6³ + 8³ is 9³ − 1, and 9³ + 10³ is 12³ + 1. Close, but never equal. Andrew Wiles, with a final step completed with Richard Taylor, proved the theorem in 1995. So this is known mathematics, and no new theorem is claimed.

In episode AN01, we covered Anthropic’s first Lean formalization, released on September 4. Dozens of agents running an unreleased research model worked for 11 days on Prove2Me, a purpose-built platform, with occasional instructions from a researcher, Tianyi Peng. They wrote about 13 million lines of Lean, using about 6 billion output tokens. That code is public. A comparator matched its statement to Mathlib’s, and Kevin Buzzard compiled it and ran the check himself.

On November 9, 2026, Anthropic announced two new models, Claude Fable 5.2 and Claude Mythos 5.2. One paragraph returns to Fermat. It says a team of 1,000 Fable 5.2 agents fully formalized the theorem in just 30 hours, with “minimal human intervention”. It says they started from minimal prompts, built their own coordination, and used “no mathematical references”, only a list of intermediate statements to score progress. Compared with the first formalization, it says, they needed one-third as many action tokens and produced a proof seven times shorter.

What the companion documents add

Two companion documents, also from Anthropic, add detail. A blog post on claude.dev, by five authors including Peng, calls it a toy experiment, run on an early version of Fable 5.2, which reproduced the proof in 28.7 hours. The system card calls the model an earlier snapshot. And the starting point was larger than the announcement’s one line suggests: 60 statements to prove, each with a one-line description, a one-sentence sketch of the classical route, the definitions those statements use, 47 proved lemmas from the September formalization, and Lean’s Mathlib library. The blog calls the tokens output tokens, and says there was no other guidance on how to prove the theorem or organize the work.

No new theorem: this formalizes known mathematics (Wiles, 1995, with Taylor), and the blog calls it a toy experiment that reproduced the proof.

Where it stands

Announced by Anthropic
In its Claude Fable 5.2 and Mythos 5.2 announcement, November 9, 2026, with a claude.dev blog post (five authors) and the system card (section 8.12.3).
Lean code public
No, as of November 9, 2026. None of the three documents links a repository; the September repository, anthropics/fermats-last-theorem, has not changed since September 24; we found no new Anthropic repository for this run.
Independent check
None named, and no expert reaction found. The announcement’s footnote 4 says the external organizations it names (its pre-release safety evaluators) did not review the post or the system card. The system card says Anthropic’s own grader accepted the proof using only Lean’s standard axioms.
Under expert review
Not yet
Peer reviewed
No (there is no paper).
Lean proof to inspect
None yet: the top-level statement, the axioms and the “seven times shorter” claim cannot be checked. Not built or run by us.

Last checked November 10, 2026. Where it stands. As of November 9, no Lean code from this run is public. The announcement links no repository, the September repository has not changed since September 24, and we found no new Anthropic repository for it. So no one outside can yet check the top-level statement, the axioms, or the proof seven times shorter; the documents do not say whether length means lines, or whether the 47 supplied lemmas count. The system card says Anthropic’s grader accepted the proof using only Lean’s standard axioms. But Lean’s kernel checks proofs, not whether a statement says what Fermat said. We found no outside expert reaction yet. A footnote says the outside safety evaluators did not review the post or the system card; they tested safety, not mathematics, and no outside mathematician is named either. Nothing is peer reviewed, and none of it was built or run by us.

How the two efforts differ, on stated facts. AN01: an internal research model, dozens of agents on a purpose-built platform, a researcher’s occasional guidance, 11 days, public code with an outside check. AN04: an early version of a released model, 1,000 agents with general tools, starting from the first formalization’s definitions and lemmas, under 30 hours, and no code yet. Both formalize known mathematics, and this one is benchmarked only against Anthropic’s own earlier run and its everyday model. If the code is published and holds up, agents will have redone in 30 hours, starting from the September run’s definitions and lemmas, what first took 11 days. Until then, it is Anthropic’s claim, with detailed accounts but no code. See AN01.

How the run went

  1. The run. How the run went, in the blog’s account. One lead agent and 999 helpers, each in its own sandbox with no internet, shared only a Git repository and a database. In its first 10 minutes, the lead set up 5 tables and dealt out the 60 statements, 16 or 17 helpers to each. Three were proved by minute 27. Most helpers judged 47 others infeasible in the time available, so the lead moved nearly everyone onto the remaining 10, which were proved within about 70 minutes, and then back onto the hard ones. The hardest, the Langlands–Tunnell theorem, drew about 750 helpers and a tree of 2,418 tasks, up to 10 levels deep. It was proved at hour 28.4, and the final theorem at hour 28.7. By the blog’s count, fifty-four of the 60 statements were proved: five alternatives were no longer needed, and one was dropped.
  2. The people and the comparison. Minimal human intervention, concretely. People built the harness, wrote the prompt and chose the 60 statements. The harness sent the lead 19 automatic reminders of the time left, each urging it to keep going. The system card’s runs had an 18-hour budget; at hour 18, Anthropic resumed both teams from their last save with 12 more hours. The blog says no researcher steered the work during the run. The comparison is Anthropic’s own. In what it calls the same 1,000-agent setup, Opus 5.5, which Anthropic recommends for everyday work, a tier below Fable, had 26% at hour 18 and 27% at hour 30, against 86% and then a complete proof for Fable. Each model had a single run, and progress is a weighted share of the 60 statements, scored by Anthropic’s own grader.

The numbers in the video

  • Ours: 6³ + 8³ = 728 = 9³ − 1 and 9³ + 10³ = 1729 = 12³ + 1; a small search finds no solution of aⁿ + bⁿ = cⁿ for n = 3 to 10 with c ≤ 300 (an illustration, not a proof).
  • Ours: 11 days = 264 hours, so the bars in the video are drawn at 264 : 30; 999 helpers over 60 statements is 16.65 each (“16–17”, blog); 60 − 3 − 47 = 10.
  • Announcement chart (single run per model, weighted share of 60 statements): Fable 5.2 0.86 at hour 18 and 1.00 by hour 30; Opus 5.5 0.26 at hour 18 and 0.27 at hour 30.
  • Blog: 1 lead and 999 helpers; 19 automatic reminders; restart near hour 18 with 12 more hours; Langlands–Tunnell at hour 28.4 (2,418 tasks, up to 10 levels, about 750 helpers), the final theorem at hour 28.7; 54 of 60 statements proved (five alternatives no longer needed, one dropped).
  • The token and length ratios (one-third, one-seventh) are Anthropic’s; neither document gives a unit or an absolute figure, and with no code public we could not measure them.

Read the source

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

Transcript

Read the full script

0:00The question

This is AN04. Before we start: Anthropic makes Claude, which helps make this series. This is Anthropic’s own claim: we hold it to the same standards as every other lab’s, using only public sources. Fermat’s Last Theorem says that for any whole number n of at least three, no positive whole numbers a, b and c satisfy aⁿ + bⁿ = cⁿ. Cubes come close: 6³ + 8³ is 9³ − 1, and 9³ + 10³ is 12³ + 1. Close, but never equal. Andrew Wiles, with a final step completed with Richard Taylor, proved the theorem in 1995. So this is known mathematics, and no new theorem is claimed. In episode AN01, we covered Anthropic’s first Lean formalization, released on September 4. Dozens of agents running an unreleased research model worked for 11 days on Prove2Me, a purpose-built platform, with occasional instructions from a researcher, Tianyi Peng. They wrote about 13 million lines of Lean, using about 6 billion output tokens. That code is public. A comparator matched its statement to Mathlib’s, and Kevin Buzzard compiled it and ran the check himself.

1:17The claim

On November 9, 2026, Anthropic announced two new models, Claude Fable 5.2 and Claude Mythos 5.2. One paragraph returns to Fermat. It says a team of 1,000 Fable 5.2 agents fully formalized the theorem in just 30 hours, with “minimal human intervention”. It says they started from minimal prompts, built their own coordination, and used “no mathematical references”, only a list of intermediate statements to score progress. Compared with the first formalization, it says, they needed one-third as many action tokens and produced a proof seven times shorter. Two companion documents, also from Anthropic, add detail. A blog post on claude.dev, by five authors including Peng, calls it a toy experiment, run on an early version of Fable 5.2, which reproduced the proof in 28.7 hours. The system card calls the model an earlier snapshot. And the starting point was larger than the announcement’s one line suggests: 60 statements to prove, each with a one-line description, a one-sentence sketch of the classical route, the definitions those statements use, 47 proved lemmas from the September formalization, and Lean’s Mathlib library. The blog calls the tokens output tokens, and says there was no other guidance on how to prove the theorem or organize the work.

2:45How the run went

How the run went, in the blog’s account. One lead agent and 999 helpers, each in its own sandbox with no internet, shared only a Git repository and a database. In its first 10 minutes, the lead set up 5 tables and dealt out the 60 statements, 16 or 17 helpers to each. Three were proved by minute 27. Most helpers judged 47 others infeasible in the time available, so the lead moved nearly everyone onto the remaining 10, which were proved within about 70 minutes, and then back onto the hard ones. The hardest, the Langlands–Tunnell theorem, drew about 750 helpers and a tree of 2,418 tasks, up to 10 levels deep. It was proved at hour 28.4, and the final theorem at hour 28.7. By the blog’s count, fifty-four of the 60 statements were proved: five alternatives were no longer needed, and one was dropped. Minimal human intervention, concretely. People built the harness, wrote the prompt and chose the 60 statements. The harness sent the lead 19 automatic reminders of the time left, each urging it to keep going. The system card’s runs had an 18-hour budget; at hour 18, Anthropic resumed both teams from their last save with 12 more hours. The blog says no researcher steered the work during the run. The comparison is Anthropic’s own. In what it calls the same 1,000-agent setup, Opus 5.5, which Anthropic recommends for everyday work, a tier below Fable, had 26% at hour 18 and 27% at hour 30, against 86% and then a complete proof for Fable. Each model had a single run, and progress is a weighted share of the 60 statements, scored by Anthropic’s own grader.

4:36Where it stands

Where it stands. As of November 9, no Lean code from this run is public. The announcement links no repository, the September repository has not changed since September 24, and we found no new Anthropic repository for it. So no one outside can yet check the top-level statement, the axioms, or the proof seven times shorter; the documents do not say whether length means lines, or whether the 47 supplied lemmas count. The system card says Anthropic’s grader accepted the proof using only Lean’s standard axioms. But Lean’s kernel checks proofs, not whether a statement says what Fermat said. We found no outside expert reaction yet. A footnote says the outside safety evaluators did not review the post or the system card; they tested safety, not mathematics, and no outside mathematician is named either. Nothing is peer reviewed, and none of it was built or run by us. How the two efforts differ, on stated facts. AN01: an internal research model, dozens of agents on a purpose-built platform, a researcher’s occasional guidance, 11 days, public code with an outside check. AN04: an early version of a released model, 1,000 agents with general tools, starting from the first formalization’s definitions and lemmas, under 30 hours, and no code yet. Both formalize known mathematics, and this one is benchmarked only against Anthropic’s own earlier run and its everyday model. If the code is published and holds up, agents will have redone in 30 hours, starting from the September run’s definitions and lemmas, what first took 11 days. Until then, it is Anthropic’s claim, with detailed accounts but no code.

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.