What Lean is — what it means for a machine to check a proof

A proof on paper works because a person reads it and is convinced. Lean takes a different form. You write the proposition as a type, and the proof as a term of that type. Then the machine examines whether "this term really has this type". If the type fits, the proof passes; if not, it does not.

The smallest example.

theorem two_add_two : 2 + 2 = 4 := rfl

Right after theorem comes the name, after : the proposition (the type), and after := the proof (the term). rfl is the term that asserts "computing both sides by their definitions gives the same thing". 2 + 2 computes to 4 by the definition of addition on natural numbers, the two sides agree, and that closes it.

You can attach a different proof to the same proposition.

theorem two_add_two_decide : 2 + 2 = 4 := by decide

theorem two_add_two_norm : 2 + 2 = 4 := by norm_num

What comes after by is a tactic — a program that builds the proof term on your behalf. decide closes "a proposition whose truth can be decided by a finite procedure" by computation, and norm_num closes it by computing a normal form of the numerical expression. The three theorems state the same proposition, and all of them pass the check.

A proposition with variables has the same shape.

example (a b : ℕ) : a + b = b + a := Nat.add_comm a b

example is the way to write something that is checked without being given a name. ℕ is the type of natural numbers, and (a b : ℕ) declares "take terms a, b of type ℕ". Nat.add_comm is the commutativity of addition; hand it a and b and it becomes a term of type a + b = b + a. Using a lemma has the same shape as passing arguments to a function — that is what "a proof is a term" feels like in the hand.

Lean has two layers.

The relation between these two layers is what decides where the trust in a machine check can be placed. A term built by a tactic is always checked by the kernel at the end. The kernel does not look inside the tactic, and does not trust it. It looks only at whether the term that arrived has the type.

Two things follow. A bug in a tactic does not necessarily make a proof that passed wrong — if the tactic builds a wrong term, the kernel rejects it. Conversely, a tactic failing does not mean the proposition is false. It only means that this particular tool could not build that term.

What you have to trust is narrowed down to the implementation of the kernel, the axioms we look at next, and the way the proposition itself is written. Where these two layers sit within Lean as a whole, and how the kernel reads a term, is in 13 How Lean works.

Lean's logic has a finite number of propositions that are accepted without proof — axioms. Which theorem relies on which axioms is something the machine answers.

theorem and_true_self (p : Prop) : (p ∧ True) = p := by simp

theorem em_holds (p : Prop) : p ∨ ¬p := Classical.em p

theorem half_add_half : (1 : ℚ) / 2 + 1 / 2 = 1 := by norm_num

#print axioms and_true_self
#print axioms em_holds
#print axioms half_add_half

Output:

'and_true_self' depends on axioms: [propext]
'em_holds' depends on axioms: [propext, Classical.choice, Quot.sound]
'half_add_half' depends on axioms: [propext, Classical.choice, Quot.sound]

These three are the three standard axioms of Lean and mathlib.

Up to here we are within "ordinary, widely used mathematics". All three are things that ordinary mathematics using classical logic and the axiom of choice uses implicitly. Every claim on this site that carries the Lean label stays within these three (the list is in The Lean verification bundle).

The same proposition can rely on different axioms depending on how it is proved. Putting the first three theorems side by side:

'two_add_two' does not depend on any axioms
'two_add_two_decide' does not depend on any axioms
'two_add_two_norm' depends on axioms: [propext]

rfl and decide close by computation alone, so they use no axioms. norm_num rewrites propositions along the way, so propext enters. A proof that uses no axioms is the strongest kind — and note that when no axioms are used, the output takes the different wording does not depend on any axioms, as above. If you write a check that counts axioms, it has to count this wording too, or it will miss cases.

When you want to move on with a proof still unfinished, Lean has a hole called sorry. Put it where the writing is unfinished, and the check proceeds as if that part were accepted.

theorem every_even_is_sum_of_two_primes (n : ℕ) (hn : 4 ≤ n) (he : n % 2 = 0) :
    ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p + q = n := by
  sorry

#print axioms every_even_is_sum_of_two_primes

Output (the warning comes with a file name and position):

warning: declaration uses `sorry`
'every_even_is_sum_of_two_primes' depends on axioms: [propext, sorryAx]

This is an open problem. And yet "the check passes" — because sorry sets up an axiom called sorryAx, and that axiom proves every proposition whatsoever. A theorem in which sorryAx appears says nothing.

A hole shows up in two forms: the warning declaration uses `sorry` during the check, and sorryAx in #print axioms. The first is a warning, so you miss it if you look only at errors. The second appears reliably for each theorem. So when confirming a claim you are going to make outward, use #print axioms, not the warning.

decide runs the decision procedure in the kernel. The kernel's computation is slow, and it stops when the object gets large.

theorem sum_to_199 : (List.range 200).sum = 19900 := by decide

error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

So there is a tactic called native_decide. It compiles the decision of the proposition to machine code, runs it, and accepts the result as an axiom. It is fast, and in exchange, what happened shows up plainly in #print axioms.

theorem sum_to_19 : (List.range 20).sum = 190 := by decide

theorem sum_to_199 : (List.range 200).sum = 19900 := by native_decide

#print axioms sum_to_19
#print axioms sum_to_199

'sum_to_19' depends on axioms: [propext]
'sum_to_199' depends on axioms: [propext, sum_to_199._native.native_decide.ax_1_1]

An unfamiliar name has been added. Looking inside it:

#print sum_to_199._native.native_decide.ax_1_1

axiom sum_to_199._native.native_decide.ax_1_1 : decide ((List.range 200).sum = 19900) = true

An axiom saying "the result of this decision is true" is newly set up for this theorem. The kernel does not redo the computation. In other words, what has to be trusted expands from the kernel and the three standard axioms to the compiler and the runtime environment. A mistake in the enumeration, or a bug in the compiler, becomes a mistake in the theorem as it stands.

This is why this site does not use native_decide. The Lean label also requires that this axiom does not appear.

#check @Lean.ofReduceBool

warning: `Lean.ofReduceBool` has been deprecated: in-kernel native reduction is
deprecated; assert native evaluations with axioms instead
Lean.ofReduceBool : ∀ (a b : Bool), Lean.reduceBool a = b → a = b

When you receive the result of a machine check, how much of it is the machine's word and where does the human's word begin? This is the boundary.

That it is what was meant

Propositions are written by people. Take a definition too weakly, swap the order of quantifiers, add one hypothesis. Each of these passes the check, and each makes the statement a different one. "If there is an edge, the distance is 1" and "there is an edge if and only if the distance is 1" are different propositions, and what can be proved from the first is less than what can be proved from the second. Real examples of this kind of mismatch are in 08.

That the definitions are as intended

A short example. Drop the condition "at least 2" from the definition of a prime, and you get this.

def NoSmallDivisor (n : ℕ) : Prop := ∀ d : ℕ, d ∣ n → d = 1 ∨ d = n

theorem one_has_no_small_divisor : NoSmallDivisor 1 := by
  intro d hd
  left
  exact Nat.dvd_one.mp hd

It passes. NoSmallDivisor 1 is true. Meanwhile:

theorem one_is_not_prime : ¬ Nat.Prime 1 := by decide

This passes too. The two do not contradict each other — because NoSmallDivisor is not the definition of a prime. Lean does not tell you about the condition you dropped. Confirming that a definition matches the intention is the job of the person who wrote it and the person who reads it.

Computations done outside the statement

When a result says "we narrowed the candidates down to 117 classes, and proved in Lean that those 117 classes do not satisfy the condition", Lean guarantees only the second half. That the candidates are exhausted by the 117 classes was confirmed by a separate computation, and is not inside the theorem. How to write and read so as to keep this distinction is in 09, and why the narrowing itself cannot be put into Lean is in 10.

That is why the Lean labels on this site always come with a theorem name. Follow the name and you can read the statement; read the statement and you can see where the guarantee ends.

Sources and reproduction

Next: 02 Getting started — up to checking the snippets above on your own machine. Terms are in 12 Glossary.