Primary evidence
- Formalizing Fermat's Last TheoremS2 · Official institutional · Official announcement · 2026-09-04
- Fermat's Last Theorem in Lean 4S1 · Primary research · Formal artifact · 2026-09-04
Anthropic releases a Claude-generated complete Lean formalization of Fermat's Last Theorem
Claude agents used Anthropic's Prove2Me workflow to build a dependency graph of formal subproblems and expand it into millions of lines of Lean code.
What happened?
Anthropic described the release as the first complete computer-checked formalization of Fermat's Last Theorem. The public Lean repository states the standard theorem, contains no admitted proof gaps in the built package, and reports successful checking by Lean, comparator and a second Rust Lean kernel.
Claude agents used Anthropic's Prove2Me workflow to build a dependency graph of formal subproblems and expand it into millions of lines of Lean code. The repository follows the classical Frey-Serre-Ribet-Wiles-Taylor-Wiles route and exposes the theorem graph, source attribution and reproducible verification procedures.
Why it matters
The event is important primarily as an autoformalization and proof-engineering milestone rather than a new proof of Fermat's Last Theorem. It tests whether multi-agent systems can assemble and verify a very large existing mathematical argument while preserving machine-checkable correctness.
Significance rationale: The release demonstrated unusually large-scale AI-driven formalization of a landmark modern theorem: Claude worked largely autonomously for 11 days to translate the established Wiles and Taylor-Wiles argument into a Lean artifact that can be checked by proof kernels.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H1 · Historical milestone
- Verification
- Independently corroborated
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Independently replayed
Contribution & verification
- Mathematical novelty
- Formalization of known result
- Interface
- Formal, Symbolic, Hybrid
- AI contribution
- Claude agents generated the bulk of the Lean formalization, decomposed proof obligations and iteratively repaired code against Lean feedback; proof kernels determined whether the resulting formal terms type-checked.
- Human contribution
- The underlying mathematics comes from Fermat's Last Theorem research culminating in Wiles and Taylor-Wiles, together with later expositions and open Lean libraries. Anthropic researchers designed and orchestrated the agent workflow, selected sources, integrated existing formal libraries and documented verification and attribution.
- Verification
- Independently corroborated · E3 · Inspectable artifact · Independently replayed
- Last reviewed
- 2026-09-11
Technical details
- Systems
- claude, prove2me, lean, mathlib
- Organizations
- anthropic, imperial-college-london, lean-community
- Problems
- fermats-last-theorem
- Methods
- multi-agent, autoformalization, formal-theorem-proving, lean, proof-dag
Sources & artifacts
- Formalizing Fermat's Last TheoremS2 · Official institutional · Official announcement · accessed 2026-09-10
- Fermat's Last Theorem in Lean 4S1 · Primary research · Formal artifact · accessed 2026-09-10
- FLT: Anthropic has beaten me to itS3 · Independent scholarly · Independent analysis · accessed 2026-09-10
- Anthropic AI formalizes proof of Fermat's last theorem — a milestone for mathematicsS4 · Reputable secondary · Media report · accessed 2026-09-10
- Complete Lean 4 formalization and verification toolingArtifact · Proof artifact
Verification history
- 2026-09-04 · Partially verified · E3 · Inspectable artifact
Anthropic released the full Lean artifact. Its verification documentation reports a from-scratch Lean build, a comparator replay against a stock-Mathlib challenge statement and acceptance by the independent nanoda Lean kernel implementation.
- 2026-09-04 · Partially verified · E3 · Inspectable artifact
Kevin Buzzard independently reported compiling the public code base and running comparator successfully. He also manually inspected non-proof/non-definition code for suspicious mechanisms. This supports `independently_replayed` formal assurance without by itself triggering the Chronicle's `independently_verified` editorial status.
- 2026-09-07 · Partially verified · E3 · Inspectable artifact
Nature independently reported the formalization and quoted mathematicians assessing its scale and significance. AI4Math Chronicle does not assign independently_verified status without a separate editorial review of artifact replay and mathematical faithfulness.
- 2026-09-10 · Independently corroborated · E3 · Inspectable artifact
Under the Chronicle's event-level verification semantics, Kevin Buzzard's independent compilation and comparator replay together with Nature's independent reporting substantively corroborate the core event description. This status verifies the event record and released formalization, not the ultimate mathematical correctness of every underlying dependency or claim.
Corrections
No corrections recorded.