[Lean] The Proof Checker Behind Verifiable AI
The basics of Lean, the language behind machine-checked math and verifiable proofs
An LLM can write a math proof that looks right but is wrong. For most text a wrong sentence is a nuisance, but for a proof it is fatal, because a proof only counts if every step holds. This is why people reached for Lean. Its checker either accepts a proof or rejects it, and that answer cannot be faked with fluent prose.
DeepMind’s AlphaProof reached silver-medal level at the 2024 International Mathematical Olympiad inside Lean, and in May 2026 its successor solved nine open Erdős problems, two of them unsolved for over fifty years. DeepSeek-Prover trains an open model on the same accept-or-reject signal. Axiom Math‘s prover solved all 12 Putnam 2025 problems for a perfect score, and the company raised $200 million at a $1.6 billion valuation in March 2026 to take the same guarantee from math into code. As AI writes more of the software behind banks, chip designs, and infrastructure, passing tests only checks the cases you wrote, but a machine-checked proof covers every input against a specification.
This post walks through Lean with small examples to help you understand how it works. The Lean examples in the first sections run in your browser at live.lean-lang.org.
Theorems as types, proofs as values
Lean is a programming language and a proof checker in the same tool. In Lean’s type system, 4 has type Nat and "hi" has type String. A statement you want to prove is also a type, and its proof is a value of that type. So proving a statement means building such a value, and Lean checks the proof the same way it checks that a function returns the type it promises. The simplest example is arithmetic.
theorem two_plus_two : 2 + 2 = 4 := by rflThis declaration has three pieces.
two_plus_twois the name of the declaration.2 + 2 = 4, after the colon, is the type, the statement you want to prove.by rfl, after:=, builds the value, the proof term itself (here,rfl).
So the proof is a value whose type is 2 + 2 = 4, the same way 4 is a value whose type is Nat.
rfl stands for reflexivity, and it closes any goal of the form x = x. It works here because Lean evaluates both 2 + 2 and 4, gets 4 on each side, and sees they are identical.
Most proofs are not one-liners, so you build them with tactics. A tactic transforms the current goal. At each step Lean shows you a goal state, the hypotheses you have on top and the goal you still need to prove on the bottom. The ⊢ symbol, called the turnstile, separates the hypotheses from the goal. It reads “from these hypotheses, prove what follows.” Here is a chain of reasoning everyone knows. If p implies q, and q implies r, and p holds, then r holds.
theorem chain (p q r : Prop) : (p → q) → (q → r) → p → r := by
intro hpq hqr hp
apply hqr
apply hpq
exact hpThe by keyword switches Lean into tactic mode, so each line after it is a tactic that transforms the goal. intro assumes the things you are given and names them. You choose the names, but the types come from the goal in order. The goal starts as the theorem’s type, (p → q) → (q → r) → p → r.
A function-type goal A → B is proved by assuming A and proving B, and that is what intro does, one arrow at a time, left to right. intro hpq peels off the first argument (p → q) and names it hpq, intro hqr peels off (q → r), and intro hp peels off p, leaving the goal r. (p q r : Prop are already in context because they are binders before the colon in the theorem signature.) Lean answers with the goal state as you write. The blocks below labeled Lean shows are this output, not code you type.
Lean shows:
p q r : Prop
hpq : p → q
hqr : q → r
hp : p
⊢ rThe context lists the hypotheses in the order intro named them, not the order the proof uses them. apply works backward from the goal, and you keep going backward until the goal is something you already hold. The goal is r, and hqr has type q → r, which means it produces an r from a q. So if you can prove q, then hqr gives you the r you need. apply hqr makes that move and replaces the goal r with the smaller goal q. Running apply hpq the same way replaces q with p. The goal is now p, and hp : p is already in the context, so the backward chain is done. exact hp gives that proof directly and closes the goal.
This is the whole loop of writing Lean. Read the goal state, run a tactic, watch the goal get smaller, and repeat until Lean prints “No goals.”
Proof by induction
The code looks correct but does not work.
theorem zero_add (n : Nat) : 0 + n = n := by rflLean shows:
error: Tactic `rfl` failed: The left-hand side
0 + n
is not definitionally equal to the right-hand side
n
n : Nat
⊢ 0 + n = nHere Lean cannot reach the answer by evaluating the expression. 2 + 2 reduced because both numbers were known. But Nat addition in Lean recurses on its second argument, and here the second argument is a variable n, not a concrete number. There is nothing to compute. 0 + n is stuck.
The error is not a dead end. It shows the exact goal state, and it tells you precisely what is stuck. Because n is an arbitrary natural number, you can prove the statement for every n by induction.
theorem zero_add (n : Nat) : 0 + n = n := by
induction n with
| zero => rfl
| succ k ih => rw [Nat.add_succ, ih]induction splits the proof in two, and in each branch it replaces n with one of the two ways a Nat can be built. The base case zero replaces n with 0, so the goal becomes 0 + 0 = 0. The replacement is automatic, but closing the goal is not, so you still call rfl, which now works because the second argument is a concrete 0 instead of a variable, letting the addition compute both sides down to 0. The step case succ replaces n with k + 1 and hands you the inductive hypothesis ih : 0 + k = k, the same statement already proved for the smaller k, then asks you to prove it for k + 1. rw rewrites the goal by replacing the left side of each equality you give it with the right side. Nat.add_succ turns 0 + (k + 1) into (0 + k) + 1, then ih turns 0 + k into k, leaving k + 1 = k + 1, which Lean closes automatically. Lean computes whatever it can, and you prove the rest.
Inside the induction tactic
induction n with ... follows a fixed grammar rather than being free-form text. The with keyword introduces one named branch per constructor of n‘s type, and each branch starts with |. Each branch name must match a constructor of n‘s type. #print Nat prints the type’s definition and shows where zero and succ come from.
#print NatLean shows:
inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → NatA natural number is built one of two ways. It is either Nat.zero, or it is Nat.succ applied to a smaller natural number. Those two constructors are exactly the two branches induction makes you cover, and the branch names match the constructor names with the Nat. prefix dropped.
| zero => ...handles theNat.zerocase.| succ k ih => ...handles theNat.succcase. The two names aftersuccare yours to choose.knames the smaller number sitting inside thesucc, andihnames the inductive hypothesis, the proof of the statement forkthat Lean hands you for free. The=>separates the branch from the tactic that proves it.
The Gauss sum formula
Now we will look at a more complex example and prove the formula for 1 + 2 + ... + n, which equals n(n+1)/2. We prove 2 * gauss n = n * (n + 1) instead, the same formula multiplied by 2, so we avoid dividing whole numbers.
def gauss : Nat → Nat
| 0 => 0
| n + 1 => gauss n + (n + 1)
theorem gauss_eq (n : Nat) : 2 * gauss n = n * (n + 1) := by
induction n with
| zero => rfl
| succ k ih =>
rw [gauss, Nat.mul_add, ih]
simp only [Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul]
omegaThe definition comes first. gauss takes a natural number and returns one, written by matching the two shapes a Nat can have, the same 0 and n + 1 split that drives induction.
| 0 => 0says the sum up to zero is zero.| n + 1 => gauss n + (n + 1)says the sum up ton + 1is the sum up ton, which isgauss n, plus the new numbern + 1itself.
The second line calls gauss on the smaller n, so the function adds 1, then 2, and on up. gauss 3 is gauss 2 + 3, and gauss 2 is gauss 1 + 2, all the way down to gauss 0 = 0, so it works out to 0 + 1 + 2 + 3 = 6.
Now we will go through the proof one line at a time. The induction n with splits it into the same two branches as before, named for Nat‘s two constructors.
The base branch, | zero => rfl, faces this goal.
case zero
⊢ 2 * gauss 0 = 0 * (0 + 1)gauss 0 is 0 by definition, so the left side is 2 * 0 and the right side is 0 * 1. Both compute to 0, and rfl closes it.
The step branch, | succ k ih, gets the inductive hypothesis ih : 2 * gauss k = k * (k + 1) and has to prove the statement for k + 1.
case succ
k : Nat
ih : 2 * gauss k = k * (k + 1)
⊢ 2 * gauss (k + 1) = (k + 1) * (k + 1 + 1)Closing this goal uses three small library lemmas and two tactics. Here is what each one does.
Nat.mul_addstatesa * (b + c) = a * b + a * c.Nat.add_mulstates(a + b) * c = a * c + b * c.Nat.mul_onestatesa * 1 = a, andNat.one_mulstates1 * a = a.simp only [...]applies the lemmas you list as left-to-right rewrites, over and over, everywhere they match, until none of them apply anymore.omegais a built-in tactic that proves goals about whole numbers by itself, without any lemma names from you. It works as long as the goal uses only+,-, multiplication by a constant, and comparisons like=,≤, and<. For example, it closes2 * k + 2 = 2 * (k + 1)by itself. It does not reason about two unknowns multiplied together, such asa * b. It just treats that product as a single unknown value.
Now let’s take a look at the branch one line at a time.
rw [gauss, Nat.mul_add, ih] does three rewrites in order.
gaussunfoldsgauss (k + 1)intogauss k + (k + 1)using the function’s own definition.Nat.mul_adddistributes the2across that sum, turning2 * (gauss k + (k + 1))into2 * gauss k + 2 * (k + 1).ihreplaces2 * gauss kwithk * (k + 1), the one and only place the inductive hypothesis is used.
No gauss is left, and the goal is pure algebra.
⊢ k * (k + 1) + 2 * (k + 1) = (k + 1) * (k + 1 + 1)simp only [Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul] multiplies out every product into a flat sum, the same expansion you would do by hand. On the left, Nat.mul_add turns k * (k + 1) into k * k + k * 1, then Nat.mul_one shortens k * 1 to k, leaving k * k + k. The term 2 * (k + 1) becomes 2 * k + 2 the same way. On the right, Nat.add_mul splits the leading sum in (k + 1) * (k + 1 + 1), and the same rules flatten what is left. Nothing remains but sums of single products.
⊢ k * k + k + (2 * k + 2) = k * k + k + (k + 1) + (k + 1)omega finishes. Both sides are the same quantity, k * k + 3 * k + 2, written in a different order. omega cannot reason about the nonlinear k * k, so it replaces that term with a fresh variable, the same one on both sides since the term is identical. The goal is now linear, both sides reduce to that variable plus 3 * k + 2, and the matching k * k terms cancel, so omega confirms they are equal. omega handles both the final arithmetic and the search for the right lemma names.
You have a machine-checked proof of the Gauss sum formula.
Proving a false statement
Every error so far came from an incomplete or mismatched proof. The case that matters is a proof that is structured correctly but proves a statement that is false. Suppose a model writes the Gauss formula with an off-by-one mistake, claiming 2 * gauss n = n * n instead of n * (n + 1). The induction is set up exactly like the real proof.
theorem gauss_wrong (n : Nat) : 2 * gauss n = n * n := by
induction n with
| zero => rfl
| succ k ih =>
rw [gauss, Nat.mul_add, ih]error: unsolved goals
case succ
k : Nat
ih : 2 * gauss k = k * k
⊢ k * k + 2 * (k + 1) = (k + 1) * (k + 1)unsolved goals is what Lean prints when the tactics run out while a goal is still open. This proof stops right after the rewrites, the same point where the real proof still had simp only and omega left to run. Those finishing tactics are not here, so the rewritten equation is left open with nothing to close it. This leftover goal shows the mistake. The left side k * k + 2 * (k + 1) is k*k + 2k + 2, and the right side (k + 1) * (k + 1) is k*k + 2k + 1. They differ by 1.
Adding the simp only and omega that finished the real proof does not save it either. simp only flattens both sides, and now both carry the term k * k, which omega cancels as one shared variable the same way it did before. What remains is 2 * k + 2 on the left and 2 * k + 1 on the right, equal only if 2 = 1. That is false for every k, so omega cannot close the goal.
error: omega could not prove the goalThe off-by-one that began as a wrong formula ends as the plain contradiction 2 = 1, and Lean refuses it.
A rejected proof has two possible causes worth distinguishing. The statement might be true while the proof is incomplete, in which case a better proof still goes through. Or the statement is false, in which case no proof will ever go through. Lean rejects both the same way and does not tell you which case you are in from a single attempt.
For verifiable AI the ambiguity is harmless, because both rejected cases collapse to the same safe outcome. Whether the statement was false or just unproven, you are never told something untrue is true. The guarantee runs one direction. If Lean accepts a proof, the statement is true, and a false statement never earns an accepted proof, no matter how confident the model that wrote it. The checker does not grade prose or reward confident reasoning, it only certifies that each step follows.
Lean as an AI reward signal
A model can run on this same accept/reject signal as a loop. It writes a wrong proof, reads Lean’s error, and fixes it. That is the loop AlphaProof and DeepSeek-Prover run at scale, where the reward is “did Lean accept it.” Here is a three-round run on a simple problem. sum adds up a list of numbers, and the goal is to prove that summing two lists separately and adding the totals equals summing them joined together. For example, sum [1, 2] + sum [3] equals sum [1, 2, 3], both 6.
In the first round, the model tries by rfl:
def sum : List Nat → Nat
| [] => 0
| x :: xs => x + sum xs
theorem sum_append (xs ys : List Nat) : sum (xs ++ ys) = sum xs + sum ys := by rflsum matches the two shapes a list can have, the same way gauss matched 0 and n + 1. | [] => 0 says the empty list sums to zero. | x :: xs => x + sum xs says a list whose first element is x and whose rest is xs sums to x plus the sum of the rest. The :: builds a list from a head and a tail, and ++ joins two lists.
The proof attempt hits the same stuck-on-a-variable error as 0 + n. Lean cannot compute sum (xs ++ ys) because xs is a variable, so xs ++ ys is stuck and there is nothing to reduce.
Lean shows:
error: Tactic `rfl` failed: The left-hand side
sum (xs ++ ys)
is not definitionally equal to the right-hand side
sum xs + sum ys
xs ys : List Nat
⊢ sum (xs ++ ys) = sum xs + sum ysThe model reads it and switches to induction on the first list. Round 2 covers both cases but leaves the arithmetic in the step unfinished.
theorem sum_append (xs ys : List Nat) : sum (xs ++ ys) = sum xs + sum ys := by
induction xs with
| nil => simp [sum]
| cons x xs ih => rw [List.cons_append, sum, sum, ih]The base case is not free this time. sum ([] ++ ys) reduces to sum ys, but the other side reduces to 0 + sum ys, which is stuck on a variable for the same reason 0 + n was. Plain rfl cannot close it, so simp [sum] does. simp rewrites the goal using sum‘s own equations plus Lean’s built-in simplification lemmas, which include 0 + n = n, until both sides match. The step case is named cons after the list constructor that builds a nonempty list from a head x and a tail xs, the list version of Nat‘s succ. The rw chain unfolds the goal one rewrite at a time. List.cons_append turns (x :: xs) ++ ys into x :: (xs ++ ys). The first sum unfolds the left side, sum (x :: (xs ++ ys)), into x + sum (xs ++ ys). The second sum unfolds the right side, sum (x :: xs), into x + sum xs. There are two because sum is applied to a nonempty list in two places, once on each side of the equation. Finally ih replaces sum (xs ++ ys) with sum xs + sum ys. What is left is pure arithmetic with nothing to close it.
Lean shows:
error: unsolved goals
case cons
ys : List Nat
x : Nat
xs : List Nat
ih : sum (xs ++ ys) = sum xs + sum ys
⊢ x + (sum xs + sum ys) = x + sum xs + sum ysThe leftover goal is precise. The left side x + (sum xs + sum ys) and the right side x + sum xs + sum ys are the same number grouped differently. The fix is to add omega to the end of the step branch and change nothing else. omega is the right tool because the leftover is linear arithmetic, only additions of unknown numbers regrouped, which is the kind of goal it closes on its own:
theorem sum_append (xs ys : List Nat) : sum (xs ++ ys) = sum xs + sum ys := by
induction xs with
| nil => simp [sum]
| cons x xs ih => rw [List.cons_append, sum, sum, ih]; omegaLean accepts the proof. Each error pointed at the exact remaining goal, so the loop converged. That binary signal is what lets Lean work as both a verifier and a reward function.
DeepMind released AlphaProof’s accepted proofs for IMO 2024. Problem 1 asks you to find every real number α for which ⌊α⌋ + ⌊2α⌋ + ... + ⌊nα⌋ is a multiple of n for every positive integer n. The answer is the even integers. The whole problem is one Lean theorem.
theorem imo_2024_p1 :
{α : ℝ | ∀ n : ℕ, 0 < n → (n : ℤ) ∣ ∑ i in Finset.Icc 1 n, ⌊i * α⌋}
= {α : ℝ | ∃ k : ℤ, Even k ∧ α = k} := by ...Its proof is 138 lines of code no human would write by hand. A typical line looks like this:
existsλx L=>(L 2 two_pos).rec λl Y=>?_AlphaProof searches an enormous space and emits 138 lines, and the same small kernel that checks a one-line human proof accepts them. AlphaProof, DeepSeek-Prover, and Axiom Math all run this accept-or-reject loop with search and learning added on. They turn an English problem into a Lean theorem, propose a candidate, and learn from the one bit the kernel returns. The kernel never lowers its standard, so the reward can never be gamed. This is also why a fixed checker draws interest from people working on self-improving AI, where a model trains on its own output.
Inside the kernel
Whatever the tactics, the elaborator, and the AI on top produce is a fully spelled-out proof term, and every one of them goes to the kernel, a small program in C++. The kernel switches on the shape of a term.
switch (e.kind()) {
case expr_kind::Lit: r = lit_type(lit_value(e)); break;
case expr_kind::MData: r = infer_type_core(mdata_expr(e), infer_only); break;
case expr_kind::Proj: r = infer_proj(e, infer_only); break;
case expr_kind::FVar: r = infer_fvar(e); break;
case expr_kind::MVar: throw kernel_exception(env(), "kernel type checker does not support meta variables");
case expr_kind::BVar: lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Sort: /* check_level, then */ r = mk_sort(mk_succ(sort_level(e))); break;
case expr_kind::Const: r = infer_constant(e, infer_only); break;
case expr_kind::Lambda: r = infer_lambda(e, infer_only); break;
case expr_kind::Pi: r = infer_pi(e, infer_only); break;
case expr_kind::App: r = infer_app(e, infer_only); break;
case expr_kind::Let: r = infer_let(e, infer_only); break;
}A Lean term is one of about a dozen shapes, a function, an application, a constant, a sort, a literal. To find a term’s type the kernel looks at its shape and handles each case. That is type inference with no hidden machinery. The MVar case throws an error. A metavariable is an unsolved blank the elaborator uses while building a proof, and the kernel refuses to look at one. By the time a term arrives, every blank must be filled.
Accepting a theorem is the second piece.
type_checker checker(*this, diag.get());
// ... val = the proof term, type = the statement we claim to prove ...
if (!checker.is_prop(type)) // the statement must be a proposition
throw theorem_type_is_not_prop(*this, v.get_name(), type);
check_no_metavar_no_fvar(*this, v.get_name(), val); // no blanks left
expr val_type = checker.check(val, v.get_lparams()); // infer the proof term's type
if (!checker.is_def_eq(val_type, type)) // does the proof actually prove it?
throw definition_type_mismatch_exception(*this, d, val_type);A proof is a value, a theorem is its type. To accept a theorem the kernel infers the proof term’s real type and checks it equals the claimed statement with is_def_eq. Only then is it recorded. “Checked” means exactly “this term’s type is the theorem you claimed.”.
is_def_eq is the last piece, the reason rfl could close 2 + 2 = 4.
bool type_checker::is_def_eq(expr const & t, expr const & s) {
bool r = is_def_eq_core(t, s);
if (r)
m_st->m_eqv_manager.add_equiv(t, s); // cache the result
return r;
}It answers whether two types are the same after computation. Two terms can look different and be equal once evaluated, like 2 + 2 and 4. The kernel reduces both sides and compares.
How induction becomes a term the kernel runs
You might expect induction to need its own machinery inside the kernel. It does not, and that is part of why the kernel stays small. The induction n with | zero => ... | succ k ih => ... never reaches the kernel as a tactic. The tactic runs outside the trusted base. It turns your two branches into a plain term, a call to a function named Nat.rec that takes the two branches as its arguments. Nat.rec is generated automatically for Nat. Lean creates one such function, called the recursor, for every inductive type, and it is the function that runs recursion over the values of that type. The kernel only ever sees that finished term. It runs the term by reading which constructor built n and selecting the branch with the same name. The step is called iota-reduction.
optional<recursor_rule> get_rec_rule_for(recursor_val const & rec_val, expr const & major) {
expr const & fn = get_app_fn(major);
if (!is_constant(fn)) return optional<recursor_rule>();
for (recursor_rule const & rule : rec_val.get_rules()) {
if (rule.get_cnstr() == const_name(fn))
return optional<recursor_rule>(rule);
}
return optional<recursor_rule>();
}major is the number being recursed on. The loop reads the constructor that built it and finds the matching branch. Lean then evaluates that branch with the constructor’s parts and the inductive hypothesis filled in. Induction is not a special case in the kernel. It is an ordinary term whose reduction picks a branch by constructor, handled by the same case expr_kind::App as every other application.
This is the property AI labs rely on. A buggy tactic, a careless contributor, or an adversarial model cannot get a false theorem past the kernel, because the kernel does not trust how a term was produced, only the term itself.
The limits of verification
Lean guarantees that the proof proves the formal statement. It does not guarantee the formal statement matches the informal problem you meant. Translating English math into a Lean theorem, the autoformalization step, is its own source of error. If the formal statement is wrong, a valid proof does not help. So the kernel removes one failure mode completely, the invalid proof, but verifiable AI research still has open problems beyond it. Faithful autoformalization, the cost of proof search, and proving statements about real-world code rather than clean math are all active areas of work.