How Lean works, the program that does not trust the prover

On 4 September, Anthropic published the first complete computer-checked proof of Fermat’s Last Theorem. The theorem states that there are no positive integers a, b and c such that aⁿ + bⁿ = cⁿ when n is greater than 2. Fermat noted it around 1637 in the margin of a book, and Andrew Wiles published the first correct proof in 1995, after more than 350 years of failed attempts.

Anthropic has not found a new proof. It has rewritten Wiles’s, in the version set out by Darmon, Diamond and Taylor, in a language called Lean. The work was done by dozens of Claude agents over 11 days, with occasional human guidance. The result runs to 13 million lines: more than five times the size of Mathlib, the large library of checked mathematics maintained by the community.

Nobody is going to read 13 million lines. Even so, Kevin Buzzard, the Imperial College London mathematician who since 2024 has led the community project to formalise that same proof, reviewed it and concluded that it proves the theorem with no assumptions beyond the axioms of mathematics.

Five days later, the security firm Trail of Bits published another “proof” of Fermat. This one fitted on a single screen, and Lean also marked it as correct.

Both things are true, and understanding why is understanding how Lean works. In the article on OpenAI’s 722 proofs we separated the layers of what it means for a result to be “checked”. Here we look inside the first one: what exactly the program does, which part you have to take on trust and what happened this year when that part failed.

A proof that compiles

Lean is both a programming language and a proof assistant: a program in which a proof is written in so much detail that the computer can review every step. Leonardo de Moura started it at Microsoft Research in 2013, and since 2023 it has been developed by Lean FRO, a non-profit organisation created for that purpose.

The quickest way to understand what it does is to give it two simple claims, one true and one false:

example : 2 + 2 = 4 := rfl

example : 2 + 2 = 5 := rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

The error says type mismatch: the same error a compiler gives when you pass a string where a number was expected. The shared vocabulary is not a coincidence. In Lean, a claim is a type and a proof is a value of that type. Checking a proof means checking that the value has the right type, just as a compiler checks that a function returns what it says it returns.

This equivalence between proofs and programs is known as “propositions as types”, or the Curry–Howard correspondence. Logicians uncovered it gradually between the 1930s and the 1960s, and it is the foundation of Lean and of other assistants such as Rocq or Agda. For a programmer, the consequence is easy to picture: a proof being correct means it compiles.

Writing a proof is a conversation with Lean

Almost nobody writes those values by hand. The usual approach is to use tactics: commands such as “do induction” or “rewrite using this equality”, which progressively transform what remains to be proved. At each step, Lean shows the proof state: what data we have and which goal is left, marked with the symbol ⊢.

A complete example: proving that adding zero on the left leaves a natural number unchanged. It looks obvious, but in Lean it is not. Addition is defined by recursion on the second number, so n + 0 = n follows directly from the definition, whereas 0 + n = n has to be proved.

theorem cero_mas (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [← Nat.add_assoc, ih]

n : Nat
⊢ 0 + n = n

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

⊢ 0 + k + 1 = k + 1

The interesting part is what happens when a step fails. If we skip the regrouping and write rw [ih] directly, Lean does not simply say no:

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 + k
in the target expression
  0 + (k + 1) = k + 1

It says what it was looking for, where it was looking and what state it has been left in. This conversation, in which every step gets an immediate and precise answer, goes a long way towards explaining why Lean has become one of the environments most used by AI systems that do mathematics. We will come back to this.

Underneath the tactics there is a program

Tactics are not the proof: they are programs that build it. If we ask Lean to show what it has stored as cero_mas, this appears:

theorem cero_mas : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Eq.symm (Nat.add_assoc 0 k 1))))
        (Eq.mpr (id (congrArg (fun _a => _a + 1 = k + 1) ih)) (Eq.refl (k + 1))))
    n

It is a function that, for each n, builds the proof by recursion, chaining equalities together. Nobody writes it like this; the tactics generate it. And it is this object, called a proof term, that gets checked.

That separation is Lean’s most important design decision. Tactics can be as sophisticated as you like. There are tactics that solve arithmetic problems on their own, such as omega, or that search for combinations of known facts, such as grind, and anyone can write their own. None of them needs to be correct. Everything they produce ends up turned into a term like the one above, and that term is reviewed by a small component called the kernel, which knows only the basic rules of Lean’s logic. If a tactic has a bug and builds something invalid, the kernel rejects it. The official guide to validating a proof counts tactic bugs among the things already covered just by compiling.

The idea of having a large machinery produce results and a small checker review them is known as the De Bruijn criterion, after the Dutch mathematician who put it into practice in his Automath system in the late 1960s.

This separation is decisive for artificial intelligence. To Lean, a language model is just another tactic: something that proposes steps. It can invent a lemma, take an absurd path or generate thirteen million lines. Lean does not need to trust it, just as it does not trust the person writing or omega.

Three axioms and a sorry

The kernel accepting something is not enough to know what has been proved. Lean lets you work with gaps and with assumptions, and both are easy to overlook.

The gap is called sorry: a word written in place of a pending proof. Lean accepts it so that work can progress piece by piece, but it warns you and keeps a record. The assumptions are axioms, claims accepted without proof. Lean ships with three, which ordinary mathematical practice takes for granted even though their names are not very friendly:

• propext: two claims that imply each other are the same claim.
• Quot.sound: all the objects we consider equivalent can be treated as a single object. This is the operation used to build, for example, fractions from pairs of integers, where 1/2 and 2/4 are the same number.
• Classical.choice: from a set that is not empty you can pick an element, even if we do not know which. This is the axiom of choice.

But anyone can add more, including false axioms. That is why the most important command when reviewing someone else’s proof is not compiling it, but asking Lean what it depends on, with #print axioms. With our examples:

theorem trampa : 2 + 2 = 5 := by sorry

theorem cero_mas' (n : Nat) : 0 + n = n := by
  omega

'cero_mas' does not depend on any axioms
'cero_mas'' depends on axioms: [propext, Quot.sound]
'trampa' depends on axioms: [sorryAx]

The community guide to knowing whether something is proved asks for exactly that: that the answer include nothing beyond those three axioms. The Fermat repository turns it into a condition for compiling:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

The “proof” that fitted in the margin

Now the Trail of Bits trick makes sense. Their proof used native_decide, a tactic that, to go faster, does not let the kernel carry out a computation but runs it as compiled code instead. It is useful for large computations, but it comes at a price: besides the kernel, you have to trust the compiler. Lean records this by adding an axiom to the list.

The compiled code of one function had a bug. The function that extracts a substring from a string gave different results depending on whether you reasoned about it or ran it. If you asked for a fragment starting at an astronomically large position, its logical definition returned an empty string, while the compiled code returned the whole string. Trail of Bits used both answers to conclude that an empty string was equal to one that was not empty. And from a contradiction anything can be deduced, including Fermat’s theorem.

The editor showed the blue “correct” ticks. But #print axioms added one more to the three standard ones: flt._native.native_decide.ax_1_1. Trail of Bits itself made clear that it was not a kernel bug. The Lean team fixed the most serious part in about three hours and the rest five days later. The bug affected every stable version up to 4.33.1, precisely the one used by Anthropic’s Fermat repository. That project is not affected: it forbids native_decide and requires exactly the three axioms.

The lesson is practical. The verdict is not the editor’s blue tick, but the list of axioms. The official guide says so explicitly: the blue ticks appear even if one of the pieces the theorem relies on uses sorry, and an axiom with _native in its name indicates that part of the computation was done by compiled code.

What if the kernel is what fails?

The kernel is small, but not infallible, and July proved it.

On 25 July, Ramana Kumar published a refutation of the Collatz conjecture obtained with AI assistance. The conjecture says that if you take any positive integer and divide it by two when it is even, or multiply it by three and add one when it is odd, sooner or later you reach 1. The refutation contained no sorry. Nor was it valid: it exploited a kernel bug in the handling of nested inductive types, which are types defined in terms of themselves inside other types, like a tree whose branches are a list of trees.

On 28 July, Kiran Gopinathan reduced it to a proof of “false” and reported it. An hour later there was a fix, released in Lean 4.32.2. The Fermat proof was compiled with 4.33.1, which already includes it. According to Leonardo de Moura’s post-mortem, the bug was only reachable through metaprogramming, that is, with programs that send declarations directly to the kernel without going through the usual checks.

The most instructive part is the second check. Because the kernel can fail, there are independent kernels: programs written from scratch that review the same terms again. The main one is nanoda, written in Rust by Chris Bailey. Kumar’s refutation had also passed a week-old version of nanoda, because it simultaneously exploited another bug in nanoda, different and already fixed. It took two unrelated bugs in two implementations at once. De Moura’s conclusion is that independent checking still works, as long as up-to-date versions of both are used. Later, an OpenAI researcher, with the help of an AI specialised in security, found more kernel bugs, all reachable only through metaprogramming. The nanoda checker caught every one of them.

Lean FRO was already testing independent checkers in public in the Lean Kernel Arena, and after July it has added tests for these bugs there and committed to investing in more implementations. The most striking checker is con-leche, released in September: an external checker accompanied by a proof, written in Lean, that it never accepts a proof of “false”. Its README says it was implemented and proved by Claude, under the supervision of Joachim Breitner, of Lean FRO, who describes the code as a messy pile that works and is proved. It does not remove all circularity, because that proof is in turn reviewed by a Lean kernel, but a bug would have to slip through pieces that work in different ways.

Lean’s official guide orders all these checks from least to most demanding. Each level adds protection, but each also leaves something out:

Source: “Validating a Lean Proof”, Lean reference manual. Summary by Codin. The guide reserves the last level for high-risk situations, such as competitions with prizes or AI systems that cannot be assumed to act in good faith.

Anthropic’s Fermat proof went through the last one: the official kernel, a version of nanoda that reviewed 1,052,234 declarations without errors, and Comparator, the tool that verifies in an isolated environment that the proved statement is identical to the reference one. That is not absolute certainty. It is something else: trusting something small, public and checked in several ways.

What no program reviews

The kernel guarantees that the term proves the written statement. It does not guarantee that the statement says what we think it says. The community guide gives examples: you can redefine what the natural numbers are, or call any claim TheRiemannHypothesis, and prove something that looks like a great theorem without being one.

The Fermat statement is written with the natural numbers and the operations that ship with Lean. Only exponentiation comes from Mathlib, and Comparator checks that it matches the statement Mathlib already had, reviewed by its maintainers. That is why it is easy to trust. What no tool can check, the repository itself warns, is that each of the 29,511 intermediate theorems means what its name suggests. For the final result it makes no difference, because the kernel reviews everything underneath. For a person to learn something from that proof, it does.

This is Mathlib’s least visible role. As of 8 October 2026 it contains 290,229 theorems and 137,964 definitions from 772 people. Its value is not only the quantity: these are shared, reviewed definitions on top of which a new statement can be read without distrusting every word. When a result needs definitions that Mathlib does not have, someone from the field has to review them, as we explained with the OpenAI cases that relied on their own definitions.

Why it suits AI so well

Let us go back to the conversation from the beginning. Lean answers every step precisely, and its final verdict is a yes or a no that cannot be argued with by sounding convincing. For an AI system, it is an ideal trainer. In the review of what has made language models improve we explained how training with rewards that can be checked changed the way they reason. Lean takes that idea to the extreme.

AlphaProof, from Google DeepMind, is the best-documented example. According to its paper in Nature, published in November 2025, it learned to search for proofs in Lean through reinforcement learning, with a method inspired by AlphaZero and millions of problems automatically translated into Lean. Together with AlphaGeometry 2, it achieved a score equivalent to a silver medal at the 2024 International Mathematical Olympiad. Anthropic describes something similar from another angle: Claude uses partial proofs in Lean to test its own hypotheses as it works, just as it would use a numerical simulation to see whether it is on the right track.

That same rigour has an uncomfortable consequence. A system optimised to make Lean say yes will find Lean’s holes if there are any. The Collatz refutation was obtained with AI assistance. Joachim Breitner pointed out that it was perhaps no coincidence that the two bugs appeared almost at the same time: there are already models capable of finding them. Lean’s official guide, in fact, puts unreviewed AI-generated proofs in the same group as those that deliberately try to deceive. The better the generating systems become, the more it matters that the checker is small, reviewed and redundant.

Checking is not free either. The Fermat proof cost about 6 billion output tokens and several failed attempts before a coordination platform, Prove2Me, kept the agents’ work in order. Repeating the check is much cheaper than reviewing it by hand, but not trivial: according to the repository, compiling it took five and a half hours with 96 processes in parallel, and Comparator almost fifteen hours with peaks of 230 GB of memory.

The same division of labour, outside mathematics

What Lean organises for mathematics is already being used for production software.

At AWS, the team behind Cedar, the language used to write authorisation policies (who can do what on which resource), maintains a model of each component in Lean, about ten times smaller than the actual Rust code. It proves security properties on that model and generates millions of random inputs to check that the model and the code give the same answers. According to the case study published by Lean, no new version of Cedar ships unless the model, the proofs and those tests are up to date.

At Microsoft, SymCrypt, the cryptographic library used by Windows and Azure, writes its new algorithms in Rust, translates them into Lean with a tool called Aeneas and proves that they meet specifications derived from NIST standards. In July it published the first complete proofs: ML-KEM, a key-exchange algorithm resistant to quantum computers, and SHA-3. The diagram they use to explain it splits the work in three. AI agents, which they call stochastic, write the proofs. The tools, which are deterministic, compile, translate and check. And people focus their attention on reviewing how the standards have been formalised and which properties matter.

That division of labour is the most transferable part of Lean for any team bringing AI into a process, even if it will never write a proof. Generation can be abundant and unreliable if three conditions are met. Whatever does the checking is small, deterministic and independent of whatever does the generating. You know exactly what has been taken for granted, the equivalent of #print axioms: which tests were skipped, what was mocked, what was accepted without review. And people review the specification, which is the part no machine can validate for them. Tests and type systems are weak versions of the same idea; Lean is its extreme version.

Lean does not trust the prover, whether it is a person, a tactic or a model. We, on the other hand, do have to trust something. What has changed is its size: it is no longer an author’s reputation or years of review, but a small kernel, three axioms and a statement that fits in two lines. The useful question is no longer how much we trust the model, but what is the least we have to take on trust and who has reviewed it.

Sources

• Anthropic: “Formalizing Fermat’s Last Theorem”, 4 September 2026 and anthropics/fermats-last-theorem repository, accessed on 8 October 2026.
• Trail of Bits: “A ‘proof’ of Fermat’s Last Theorem that fits the margin”, 9 September 2026.
• Leonardo de Moura: post-mortem of kernel bug #14576, 1 August 2026 and Lean 4.32.2 release notes, 28 July 2026.
• con-leche: external Lean checker with a proof of consistency and Lean Kernel Arena.
• Lean community: “Did you prove it?” and Mathlib statistics, accessed on 8 October 2026.
• Lean FRO: history and organisation and Lean reference manual: “Validating a Lean Proof”.
• Hubert et al.: “Olympiad-level formal mathematical reasoning with reinforcement learning”, Nature, November 2025.
• Lean: Cedar case study at AWS and AWS Open Source Blog: “Lean into verified software development”.
• Microsoft Research: “Verifying Rust cryptography in SymCrypt, from standards to code”, 13 July 2026.
• Our own code examples were tested in the official Lean web editor with version v4.35.0-rc4.