Research explained · September 7, 2026
Fermat was already proved. What changed in Claude’s 11 days?
Use a small example about even numbers to understand proofs, formalization and machine checking—and the work mathematicians still do.
01
What happened
Why revisit a result we already know?
The familiar equation 3² + 4² = 5² works with positive integers. Fermat’s Last Theorem says that aⁿ + bⁿ = cⁿ has no positive integer solutions when the integer exponent n is greater than 2. A human proof already exists. The new development turns an established, complicated argument into a form a machine can check.
On September 4, Anthropic reported an approximately 11-day Lean formalization using multiple agents, Prove2Me and an internal research model roughly comparable to Fable 5.1, with high-level human guidance. This result belongs to that research setup; it does not describe a single question in an ordinary chat window.
- Formalizing Fermat’s Last TheoremAnthropic research report · September 4The task, model setup, process and human involvement.
02
Understand formalization
Unpack the steps hidden inside “obvious”
Consider a small example unrelated to the Fermat proof: why is the square of an even integer even? A reader may accept this quickly. A complete explanation starts with the definition, expands the calculation and returns to that definition.
- State the condition
n is even: some integer k satisfies n = 2k.
- Expand the expression
n² = (2k)² = 4k² = 2 × (2k²)
- Return to the definition
2k² is an integer, so n² is twice an integer too.
Our teaching example illustrates conditions and steps. It is neither Lean code nor a proof of Fermat’s Last Theorem.
03
Who checks
Producing a proof and checking it are separate steps
Lean’s kernel checks proofs against formal rules. A person or an AI can produce the proof; confidence in the prose does not determine acceptance. Complex proofs also depend on definitions and earlier theorems, whose connections must be made explicit.
It also matters whether the checked statement is the intended one. The repository’s FinalCheck file gives the final statement and an axiom check; its README describes comparison with Mathlib’s statement. We read these files at a fixed revision without recompiling the large proof locally.
- Theorem Proving in Lean 4Official Lean tutorialHow the proof assistant and checking kernel work.
- FinalCheck.leanResearch repository · pinned revisionFinal statement and axiom check; we did not rerun the build.
- READMEThe team’s verification recordVerification methods, resource requirements and reading entry points.
04
The human work
A checkable proof still needs an explanation
In his own article, mathematician Kevin Buzzard reports compiling the code and running comparator successfully. His project also includes contributing modern number theory to the shared mathematics library and making the proof explorable by people. Completing a large formalization does not automatically complete those tasks.
That distinction helps explain the significance. Making intricate reasoning checkable is progress. Explaining why it works and identifying reusable intermediate results remain further work. Checkability and human understanding are both valuable goals.
- FLT: Anthropic has beaten me to itKevin Buzzard’s response · September 4His verification account and the mathematical and explanatory work that remains.
05
What to explore next
Follow one question further
Start with the research report and Buzzard’s response for the story. With a mathematical background, explore how the steps connect in PROOF-PATH. The repository includes browser-readable material; a full build needs substantial computing resources. Reading need not begin with running the entire proof.
Further questions include whether these methods help check new mathematics, whether their output becomes easier to read and reuse, and which previously omitted conditions formalization exposes. This explanation introduces those questions; one case cannot answer them all.
- PROOF-PATH.mdProof path · pinned revisionConnects the argument’s steps with their theorems, for readers with mathematical background.