Anthropic: Claude Completes First End-to-End Lean Formalization of Fermat's Last Theorem

On September 4, 2026, Anthropic announced that its AI model (the Claude series) had, after roughly 11 days of principally autonomous operation, completed the first end‑to‑end, computer‑checked Lean formalization of Fermat’s Last Theorem (FLT). This work does not represent an AI rediscovery of the mathematical proof; rather, it translates the existing human proof (largely based on Andrew Wiles’s 1995 proof and subsequent expositions) into a form that the Lean proof assistant can verify step by step. The final artifact contains approximately 13 million lines of Lean code, proves about 30,300 theorems, of which roughly 29,500 intermediate theorems are incorporated into the full proof, and it relied only on Lean’s three standard axioms. The related code has been open‑sourced on GitHub. Anthropic

Details: from years of human effort to 11 days of AI work

Fermat’s Last Theorem states that for integer exponent n>2, there are no positive integers a, b, c that satisfy a^n + b^n = c^n. Wiles’s proof published in 1995 spans roughly 100⁠–⁠129 pages and underwent months of human verification. Fully formalizing such modern mathematical proofs (i.e., writing them as code that a computer can check step by step) has long been considered a daunting task. A community project led by Kevin Buzzard at Imperial College London had planned to use several years to formalize FLT in Lean; the project blueprint itself runs to dozens of pages.

Key milestones from the Prove2Me plan that Claude used to formalize Fermat’s Last Theorem. The three colored sections correspond to three core sub‑theorems that Claude had to prove on the way to its final goal. This graph closely follows Wiles’s original proof.

Anthropic researchers led by Tianyi Peng tested Claude’s capability for automated formalization. Using a multi‑agent collaboration framework (combined with tools such as Prove2Me), dozens of Claude agents cooperatively defined concepts, proved intermediate lemmas, and incrementally advanced more complex propositions. The process consumed about 6 billion output tokens and the model operated largely autonomously for about 11 days, producing a complete, machine‑checkable proof. The formalization is over five times the size of the existing Mathlib library, making it the largest Lean proof to date.

For verification, the proof was checked by the Lean kernel; a comparator confirmed that its statements match the FLT formulation in Mathlib and that no additional axioms were introduced. The GitHub repository provides the full code, documentation of the proof path, and a browsable HTML version.

It should be emphasized that this is a formalization (translating an existing proof into machine‑verifiable code), not an AI independently discovering a new proof or new mathematical results. The original insights and proof structure of human mathematicians remain the foundation.

Potential impact on the mathematical community

1. Accelerating formalization of mathematical literature
2. Buzzard commented that if FLT can be automatically formalized, it represents a major step toward automating the formalization of modern mathematical literature. This could enable systematic checking for errors in existing papers, reduce peer‑review burden, and provide a firmer, machine‑verifiable foundation for future research.
3. Changing how proofs are verified
4. Traditionally, complex proofs rely on expert human review, which is time‑consuming and error‑prone. Machine‑checked formal proofs offer higher certainty, especially for long proofs and cross‑disciplinary results. The FLT case shows AI can handle a scale previously thought to require years of human effort.
5. New tools and collaboration models
6. Division of labor among multiple agents, construction of intermediate‑lemma libraries, and integration with existing Mathlib demonstrate a viable path for AI‑assisted formalization. Mathematicians may shift toward a “high‑level guidance + AI handles details” workflow, focusing more on conceptual innovation than tedious formalization.
7. Broad effects on mathematical practice
8. If automated formalization becomes widespread, reproducibility and trust in mathematics could increase significantly, while education, publication, and collaboration practices may change. Some foundational, verification‑oriented tasks could become largely automated.

Human concerns and reflections on AI

This breakthrough also intensifies discussion about the boundaries of AI capability:

• The line between “understanding” and “execution”

AI can translate complex human proofs into machine‑verifiable code, but does that mean it “understands” mathematics? A more accurate description today is powerful pattern matching, planning, and code generation rather than human‑like conceptual insight. Nonetheless, when AI can autonomously complete formalization work that previously required expert teams years to accomplish, the distinction becomes blurrier.

• Impact on the role of mathematicians

If verification and formalization are largely automated, mathematicians’ core value may concentrate on posing new problems, building new frameworks, and offering creative insight. Some worry that “proof factory” workflows could dilute the humanistic and exploratory character of mathematics.

• Reliability and dependence risks

Although the Lean kernel provides strong checks, whether the vast number of AI‑generated intermediate steps are entirely trustworthy and free of subtle errors requires ongoing independent review. Overreliance on AI could introduce new systemic risks.

• Broader AGI and employment anxieties

The FLT formalization is seen as a milestone for AI in rigorous logical domains, reinforcing narratives that AI is rapidly entering high‑cognitive fields and raising further debate about the future of research, education, and knowledge work.

Conclusion

Anthropic’s use of Claude to complete an end‑to‑end Lean formalization of Fermat’s Last Theorem in 11 days is a landmark for automated theorem proving and AI‑assisted mathematics. It demonstrates that current large models can execute complex, long‑duration, high‑rigor tasks far beyond prior expectations, while building on existing human proofs. For the mathematical community, it heralds a powerful new tool and prompts reevaluation of research paradigms and human roles; for the public, it underscores that AI is changing how knowledge is produced and verified, bringing both opportunities and concerns that must be addressed in parallel.

The full formalization has been open‑sourced, and independent verification and subsequent applications by the mathematics and computer science communities will determine the work’s ultimate historical significance.

▶️ Enjoyed this article? Creating content is hard!

Follow our YouTube channel:
AI Rosetta

Your likes, subscriptions and shares are our biggest support! 🙏

More AI news at: https://www.airosetta.com