Lean theorem prover/Explainers/The small trusted core

Technical version: The Lean kernel

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Lean is a large program, and large programs have faults. Yet a proof Lean accepts can be believed without believing all of Lean. This page says why: one small part does the judging, and everything else only proposes. It names the principle behind that design, the part of Lean that does the judging, and what the rest of Lean is for.

A large program with a small judge

A proof assistant has to do many things. It reads what a person types, fills in what the person left out, runs automation that searches for proofs, shows the state of an unfinished proof, reports errors and keeps track of thousands of definitions and theorems. Each of these is a place where a mistake in the program could hide.

If a proof were only as reliable as all of that machinery together, nobody could say how reliable it was. The answer is to separate two jobs. Finding a proof is hard and needs cleverness, so it is left to parts of the program that may be clever and may be wrong. Checking a proof that has been written out in full is mechanical, so it is given to a part that is simple and is meant to be right.

The second part is the only one whose mistakes would matter. If it is small, people can read it, others can write it again independently, and its correctness can itself become a subject of proof.

De Bruijn's criterion

The idea is N. G. de Bruijn's, whose Automath was the pioneer among computer systems for checking mathematics (see Automath). He stressed that checking formal proofs by machine brings a real gain in reliability, because the program that checks them can be small. Henk Barendregt and Freek Wiedijk, writing in 2005, state the principle under his name: a proof assistant meets the de Bruijn criterion when its proofs can be checked independently by a small program, one that a mathematician or logician can inspect in the usual way.

The criterion rests on a difference between proving and checking. Whether a statement has a proof at all cannot, in general, be settled by a machine. Whether a given text is a proof of a given statement can be: the checker only has to confirm that each step follows one of a small number of rules. A proof may run to megabytes; the program that checks it can still be short.

Pollack made the same argument in 1998. A simple checker that only verifies explicit derivations, with no search and no heuristics, is a formal object much smaller and easier to understand than almost any substantial proof. To believe a proof it accepts, a reader has to understand the checker, not the proof. He also recalls a remark of J Moore about an earlier prover, NQTHM: until one long proof was checked with it, a reader who wanted to believe everything it had checked would have done better to read all the proofs than its code, because the code was longer than all of them.

The Lean kernel

In Lean the judge is the Lean kernel. Lean's own reference describes it as "a small, robust implementation of a type checker for the core type theory", written in C++. Every new definition, theorem or inductive type has to pass it before it is added to Lean's environment, its table of definitions and theorems; the check is there to catch faults in the parts of Lean that produced the definition. The paper that introduced Lean 4 describes the same design: the trusted part of Lean is relatively small, and an interface lets users export their work and write their own checkers.

The Lean kernel is kept small partly by what it leaves to others. It does not search for proofs. It does not work out missing pieces of a term; that is finished before a term reaches it. It does not check that recursive functions finish: by the time a recursive definition reaches the Lean kernel, it has been rewritten into a form built from basic recursion principles, which always finish. (See functions that always finish.)

The untrusted helpers

Everything else in Lean is a helper. The elaborator turns what a person writes, with its notation, its omitted arguments and its overloaded numerals, into a complete and explicit term. Tactics are small programs that construct proof terms step by step, some of them doing a great deal of search. Neither has to be trusted for the soundness of a proof, because neither has the last word: their output goes to the Lean kernel, which accepts it or refuses it.

The difference is visible. Here a tactic, rw, proves that addition can be done in either order, and #print shows what was actually stored as the proof:

theorem swap (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

#print swap

Lean 4.34.1 prints:

theorem swap : ∀ (a b : Nat), a + b = b + a :=
fun a b => Eq.mpr (id (congrArg (fun _a => _a = b + a) (Nat.add_comm a b))) (Eq.refl (b + a))

The command rw is gone. What remains is a term made of named facts and rules, and it is that term the Lean kernel checked. If the tactic had a fault and produced a term that did not prove the statement, the Lean kernel would refuse it, and the fault would show up as an error rather than as a false theorem.

What a small core does not settle

A small judge narrows the question of trust; it does not remove it. Three things stay outside. The Lean kernel itself could have a fault, which is why independent re-checkers exist (see checking a proof again later). Some features of Lean let results in without the Lean kernel computing them; they are listed on what has to be trusted. And the Lean kernel checks that a proof proves the statement as written, which may not be the statement that was meant (see stating the right thing).

Barendregt and Wiedijk noted one more tension. Systems in which some equations are settled by computation rather than by written-out steps strain the criterion a little, since the checker must then also compute; they judged this acceptable because the basic steps of computation are themselves simple. Lean is such a system (see computation inside proofs).

Next

What has to be trusted lists everything a reader of a Lean proof still relies on. The technical counterpart, the Lean kernel, describes what it checks.