Lean Proof Assistant and AI: How Proofs Become Machine-Checkable

Eleven days, a swarm of agents, 13 million lines of code: an AI has made the proof of Fermat's Last Theorem machine-checkable. What mattered most was not computing power but a checker that lets no error through.

Around 1637, Pierre de Fermat jotted a claim in the margin of a book, for which he supposedly had a proof. It was never found. It took until 1995 for Andrew Wiles to publish a complete proof. On 4 September 2026, Anthropic announced that a swarm of Claude agents had fully formalized this proof in the proof language Lean. This was made possible by the Lean proof assistant, which checks every step of a proof by machine.

This article puts the announcement into context. It explains what a proof assistant is and why a result from Lean is considered reliable. It describes how the agents worked together and places the announcement alongside Olympiad problems and Erdős problems. Verified figures, vendor claims and open questions are kept apart. The thesis: what is new is not merely that an AI does mathematics. What is new is the combination of a model that is free to experiment and a program that rigorously signs off on every step.

Fermat's Last Theorem: what Anthropic actually announced

The theorem states that the equation aⁿ + bⁿ = cⁿ has no solution in positive integers for an exponent n greater than 2. The statement is easy to understand and was extremely hard to prove for centuries. In 1908, a prize of 100,000 gold marks was offered, and according to Anthropic, 621 false proofs were submitted in the first year alone. Wiles presented a proof in 1993, found a gap and closed it together with Richard Taylor. The publication followed in May 1995.

The latest announcement concerns the question of how certain this proof is when every step is checked by a machine. The key figures from Anthropic's publication are shown in the table.

A token is a small unit of text that a language model generates, such as part of a word. The source does not state any monetary costs. All figures come from the vendor and have not been independently recounted in this form.

The distinction is important. This is a formalization, not a new proof. The theorem had been proven since 1995. According to Anthropic, the agents built on a simplified version of Wiles's proof by Darmon, Diamond and Taylor and reused parts of the Imperial College formalization project and the flt-regular project. Anyone reading about an AI solution to Fermat's Last Theorem should therefore think of verification, not of a new mathematical discovery. Anthropic explicitly distinguishes the result from the AI work on the Riemann hypothesis, where something new was said to have been discovered.

What is the Lean proof assistant? A checker that skips no step

The Lean proof assistant is an open-source programming language that lets you write mathematical proofs in a way a computer can check. The project website lean-lang.org describes Lean as a programming language and proof assistant with a minimal, trusted kernel that guarantees correctness. Lean was developed by Leonardo de Moura and released as open source in 2013, as the Simons Foundation reports. Since 2023, the non-profit Lean FRO has been working on its further development, supported among others by 5 million US dollars from the Simons Foundation International.

The principle can be put in everyday terms. A proof in Lean is a program. Lean's kernel checks step by step whether each inference follows from the axioms and from theorems already checked. Axioms are the basic assumptions of mathematics that hold without proof. A step that does not follow is rejected, no matter how convincing it sounds. Where a proof is still missing, Lean uses the placeholder "sorry". A proof containing such placeholders counts as incomplete.

This is exactly what makes Lean so useful for AI models. Language models can phrase things convincingly and still make mistakes. In mathematics that is a problem, because an error in step 400 can invalidate everything after it. With a proof assistant like Lean, the question of whether to believe the model no longer arises.

Human peer review works differently. Experts read a proof, find it plausible and rely on their experience. That is valuable, but it takes time and leaves room for oversights. As early as 2021, a community project in Lean validated a complex proof by Peter Scholze, as the Simons Foundation describes. Checking by the proof assistant does not replace mathematical understanding, but it does provide certainty about correctness.

The process in Figure 1 shows the division of labor: the model makes proposals, the Lean kernel decides. Whether a proposal comes from a human, a model or a random generator makes no difference to the verdict.

Mathlib and the question of who checks what was checked

Lean by itself contains no mathematics. That lives in Mathlib, the community-developed library on which almost all formalizations build. The Lean website cites more than one million lines. At the time of retrieval, the community statistics page listed 139,391 definitions, 290,502 theorems and 772 contributors. Anyone proving something in Lean can draw on these verified building blocks instead of starting from scratch.

For comparison: according to Anthropic, the Fermat proof has around 13 million lines, more than five times the size of Mathlib. That sounds like a huge new construction, but it also shows how much formal verification of deep theorems costs, even when Mathlib provides the foundation. The proof depends on what has already been formalized in Mathlib.

Two verification questions must be asked separately. First: is the proof correct? Lean answers that. Anthropic states that only the three standard axioms are used. Second: was it really Fermat's Last Theorem that was proven, and not a modified statement? Here a comparator tool was used, which confirmed that the formalized statement matches the formulation in Mathlib. This separation is crucial. A flawless proof of the wrong statement would be worthless.

According to Anthropic, the complete proof, together with a written explanation, is available on GitHub for inspection. Only the model used is not public.

Kevin Buzzard of Imperial College London, who has led the formalization project since 2024, reviewed the proof. According to Anthropic, he states that the theorem is proven without assumptions other than the axioms of mathematics. One limitation remains: Lean checks correctness, not significance. The tool does not judge whether a result is interesting, elegant or important. The Simons Foundation reports corresponding assessments by Alex Kontorovich.

Agentic AI: why the swarm worked

Several dozen agents worked in parallel. In this context, an agent is a language model that does not just answer but independently uses tools, edits files and checks intermediate results. The multi-agent framework was based on Claude Code. The agents defined concepts, proved intermediate results and used them for harder statements. A general introduction is provided in the article The age of AI agents.

According to Anthropic, the breakthrough came not from a stronger model but from better organization. The Prove2Me platform, an open collaboration platform by Tianyi Peng and colleagues at Columbia University, offered three features:

• A directed acyclic graph of theorem statements provided orientation: each statement shows what it depends on, and there are no cycles.
• Statements and proofs were kept in separate files. This speeds up Lean compilation, because not everything has to be rechecked after every change.
• Theorems already proven could be searched and reused via natural-language descriptions.

Earlier attempts without this structure failed because the agents lost track of the project state. Tellingly, these attempts still contributed about 7 percent of the non-trivial lines of the final proof. The lesson: for large tasks, structure beats raw model strength. Anyone deploying many agents needs a shared plan, shared storage and clear responsibilities. Developers have the same experience with every larger agent project.

The human contribution was small, but not zero. Tianyi Peng occasionally gave high-level instructions, such as prioritizing the Jacobian variety as a scheme or finishing Mazur's theorem promptly. According to the quoted agent output, the system reported the root result as proven on 18 August at 02:00:57 UTC.

From the Olympiad to Erdős problems: AI proofs since 2024

The Fermat announcement does not stand alone. Since 2024, several results have shown that AI can prove mathematics, and they differ in whether Lean was used.

In July 2024, AlphaProof together with AlphaGeometry 2 solved four of six problems at the International Mathematical Olympiad and scored 28 of 42 points, silver level. The gold threshold was 29 points. AlphaProof proves in Lean and, among other things, solved the hardest problem of the competition. However, the problems were first translated into formal language by hand, and computing time was up to three days per problem. Contestants have two sessions of 4.5 hours.

In July 2025, Gemini Deep Think scored 35 of 42 points, gold level, officially graded by the Olympiad coordinators. The system worked in natural language within the time limit and without Lean. This is a deliberate contrast: AI becomes strong even without formal checking, but the results are then not machine-verified and must be read by humans. The company Harmonic describes in a paper on arXiv its system Aristotle, which combines Lean-based proof search with informal reasoning and a geometry solver and, according to the abstract, achieves gold-level performance on the 2025 problems.

In early 2026, the Erdős problems came into focus, a large collection of open questions posed by the mathematician Paul Erdős. One example is problem 728, whose proof by Aristotle in Lean is documented in a write-up on arXiv. According to the Simons Foundation, a 23-year-old also solved problem 1196 in early 2026 using ChatGPT and Lean.

The assessment is cautious. Terence Tao's wiki on AI contributions to Erdős problems explicitly does not see itself as a benchmark. It points to selection bias, because successes are more likely to be documented than failures. It notes that a lack of earlier progress often indicates obscurity rather than difficulty, that existing literature frequently turned up afterwards, and that a solved problem is not automatically a publishable paper. At the same time, the wiki recommends checking AI proofs formally in Lean.

The field of AI proofs in mathematics ranges from competition problems through niche problems to large formalizations. Progress is fast; whether each announcement lives up to its headline must be checked individually. That is exactly what a verification tool like Lean is for.

What are 11 days worth? A time comparison without exaggeration

The numbers invite grand comparisons. Fermat stated the theorem in 1637, Wiles proved it in 1995, a span of 358 years. The formalization project at Imperial College was launched in 2024 with an 86-page blueprint and was originally planned to take several years. The AI formalization took 11 days.

This comparison is flawed for several reasons:

• The 11 days are the runtime of an agent swarm, not the computing time of a single model.
• The proof was known. The AI did not have to find a new idea but had to translate an existing proof structure into Lean.
• There was preliminary work: Mathlib, material from the Imperial project and from flt-regular, as well as a blueprint.
• The effort of about six billion output tokens from an internal model is considerable. Monetary costs are not stated.

Equating 11 days of AI work with centuries of human work on the problem is therefore only a rhetorical comparison. What is true: work that a community project had planned over years was essentially completed in a few days.

A side experiment brings everyday use into view. According to Anthropic, three personal Claude Max subscriptions formalized Vinogradov's three-primes theorem in three days. The authors consider collaborative formalization with consumer subscriptions possible if the framework is right. That is the authors' assessment and not an independently verified result.

Limits and open points: what the announcement does not show

Anthropic itself names limitations. The proof is probably much longer than necessary, as Mathlib is more compact and better reviewed. It depends on what has already been formalized in Mathlib. The model used is an internal, non-public research model, so the result cannot be reproduced externally with the same means.

Further points remain open:

• No new mathematics was produced. The formalization increases certainty, not knowledge.
• A proof in Lean is not automatically understandable. Nobody reads 13 million lines from beginning to end.
• Lean says nothing about the significance of a theorem, only about its correctness.
• How independent the verification is beyond Buzzard's assessment is not clear from the announcement.

For further individual announcements, such as improvements on the Riemann hypothesis or autoformalization agents from individual companies, this research found no primary sources that could be checked independently. These announcements therefore remain without figures here. Assessments by individual experts are also only included where the original statement is available.

What the Lean approach means beyond mathematics

The pattern behind the Fermat project can be generalized: free experimentation on one side, strict acceptance on the other. It fits wherever a result can be checked by machine. As applications outside mathematics, the Lean website names the verification of ArkLib, a library for SNARKs (compact cryptographic proofs), and of Cedar, AWS's authorization language. In software development the principle is familiar: a compiler and a test run likewise sign off on what a human or an AI has written.

This yields a rule of thumb for dealing with AI output. The better a result can be checked automatically, the more safely a model can work freely. For texts, assessments and recommendations, this strict acceptance is usually missing. There, the human remains the checker.

The same logic applies to security and data protection: demonstrable properties count for more than mere claims. Whether a website loads trackers or sets security headers, for example, can be measured automatically. The Dr. DSGVO website check offers one way to do this, and technical security properties can be tested with the security checks. Neither are formal proofs in the Lean sense, but both follow the same idea: measure instead of believe.

Experiments by Dr. DSGVO

With the help of AI, the mathematical proof was (probably) produced and formalized that magic hexagons following a certain construction rule exist for every n (n = edge length of a hexagon made of honeycomb cells).

The total AI computing time was just under 9 hours. Of this, the system worked autonomously for practically 99.9% of the time and needed no input. The proof files totaled 173 MB! The formalization with Lean, including libraries, used almost 8 GB of disk space in intermediate steps! The whole proof stretched over a period of 5 days. It was interrupted due to usage limits and the like.

The proof will be published here soon. Whether it is correct must be judged by capable people who understand more about mathematics than the author who used AI 😉

Conclusion: the revolution is verifiability

The AI did not prove Fermat's Last Theorem anew; it fully formalized Wiles's proof in Lean, in 11 days according to Anthropic, with several dozen agents working in parallel. The success rests on two things: an organization that keeps the project state visible, and the Lean proof assistant, which only accepts what follows.

Developments since 2024 show that AI is increasingly delivering mathematical proofs. How much of it is new and how much is known material must be judged case by case, as the Tao wiki also urges. Wherever Lean is involved, correctness remains verifiable. That is the real progress: not more claims, but machine-checked certainty.