Lean is an open-source programming language and proof assistant that checks mathematical proofs line by line, and it is the tool behind this week’s most striking AI claim: that about 1,000 agents running Anthropic’s Claude Fable 5.2 fully formalized the proof of Fermat’s Last Theorem in 30 hours. The claim comes from Anthropic via press coverage and has not been independently confirmed, and the work is not peer-reviewed research we can cite. This explainer covers what Lean does, why formalization is a good test for language models and what the result would and would not mean.
What Lean is
According to its project site, Lean is an open-source programming language and proof assistant meant for correct, maintainable and formally verified code. A user writes a statement, called a theorem, and then a proof made of small, explicit steps. Lean’s kernel checks that every step follows from the rules of logic and from previously verified results. If a step is wrong, the file does not compile.
A companion effort called mathlib is a community-built library of formalized mathematics in Lean. The Lean community site describes it as a unified library of mathematics that is very active, with many regular contributors. Because new proofs can reuse mathlib’s definitions and lemmas, formalizing a result usually means connecting it to a large body of already-checked material.
What formalization means
A published proof is written for human readers. It skips steps that experts can fill in, cites other papers and relies on shared intuition. Formalization translates all of that into a form a computer can verify: every definition made exact, every skipped step spelled out and every cited result either formalized or proved again.
The result is not a new proof of the statement but a machine-checked version of an existing one. Fermat’s Last Theorem says that the equation a^n + b^n = c^n has no whole-number solutions with positive integers when n is greater than 2. Andrew Wiles presented a proof of more than a hundred pages in 1995, The Decoder notes. Formalizing it is a large undertaking because the proof relies on deep, specialized mathematics.
What Anthropic says happened
Anthropic says about 1,000 Fable 5.2 agents reached full formalization after 30 hours, translating the proof into Lean so a computer could verify it step by step. The Decoder reports an earlier, unpublished research version of Claude needed 11 days on the same task, using a purpose-built environment and guidance from a human researcher. According to Anthropic, the Fable 5.2 agents began with brief instructions, organized their own collaboration, used no mathematical references, and tracked progress only through a list of intermediate lemmas. The model used about a third of the action tokens of the first attempt and produced a proof seven times shorter.
For comparison, Anthropic ran Opus 5.5 with 1,000 agents in the same setup. Opus completed 26 percent of the formalization in 18 hours and made barely any progress through hour 30, The Decoder reports. TechCrunch adds that Anthropic says Fable 5.2 also solved two open problems in theoretical physics.
Why this is a useful test for language models
Formal proofs give a rare thing in language model evaluation: an objective judge. A model can produce text that sounds right and is wrong, but Lean either accepts a proof or does not. That makes formalization attractive for measuring long-horizon reasoning, because errors cannot hide behind fluent prose. It also makes the result easier to audit than most benchmark claims, provided the code is released.
Our earlier explainer on an AI-assisted proof of a quasi-Riemann hypothesis shows the other side of the problem: a proof written in natural language still needs expert review, while a Lean proof is checked mechanically. For more on the idea, see our glossary entry on formal verification.
What the claim does not show
- It is not a new theorem. The mathematics was already proven; the novelty is the machine-checked translation.
- It is not independent yet. The figures come from Anthropic. Until the Lean files and the setup are public, outsiders cannot check the hours, token counts or the starting conditions.
- A correct formalization still depends on the statement. Lean checks the proof of the statement as written, so reviewers must confirm that the definitions match the intended theorem.
- It does not mean general mathematical ability. Success on one well-documented target may not carry over to areas with less supporting material.
How to evaluate similar claims
- Look for the public repository and whether it compiles against a recent mathlib version.
- Check which lemmas were assumed and which were proved.
- Compare against a baseline run by the same lab, as Anthropic did with Opus 5.5.
- Ask whether humans guided the agents and how.
What to watch next
- Publication of the Lean files and the agent setup for outside review.
- Mathematicians’ assessment of the formalized statements and definitions.
- Other labs reporting comparable formalization runs.
- Use of the same method on the unfinished formalization projects in mathlib.
Key takeaways
- Lean is an open-source proof assistant whose kernel mechanically checks every step of a proof.
- Anthropic says about 1,000 Fable 5.2 agents formalized Fermat’s Last Theorem in 30 hours.
- The reported comparison: Opus 5.5 reached 26 percent in 18 hours in the same setup.
- Formalization translates an existing proof; it does not create a new result.
- The claim is lab-reported and awaits public files and expert review.
Frequently asked questions
What is Lean used for?
Lean is used to write programs and proofs that a computer can verify. Mathematicians use it with the mathlib library to formalize results, and engineers use it to check software properties.
Did AI prove Fermat’s Last Theorem?
No. Andrew Wiles proved it in 1995. Anthropic says its agents translated that proof into Lean so it can be verified by machine.
Can the Lean result be wrong?
If Lean accepts the proof, the steps are valid for the statement as formalized. The remaining risk is that the formal statement or definitions do not match the intended theorem, which is why expert review matters.
