The Lean kernel

Plain-language version: The small trusted core· What a proof assistant does

The Lean kernel is the type checker that decides whether a definition, theorem, axiom or inductive type may enter Lean's environment, its table of definitions and theorems. Everything else in Lean, from the parser to the most elaborate tactic, produces candidates; the Lean kernel accepts or refuses them. This page describes what it checks, what it never sees, how it is written, and where its trust ends, for Lean 4.34.1.

What reaches it

The Lean kernel receives fully explicit terms of one data type, Expr. With import Lean, #print Lean.Expr lists its twelve constructors:

import Lean
#print Lean.Expr

inductive Lean.Expr : Type
number of parameters: 0
constructors:
Lean.Expr.bvar : Nat → Lean.Expr
Lean.Expr.fvar : Lean.FVarId → Lean.Expr
Lean.Expr.mvar : Lean.MVarId → Lean.Expr
Lean.Expr.sort : Lean.Level → Lean.Expr
Lean.Expr.const : Lean.Name → List Lean.Level → Lean.Expr
Lean.Expr.app : Lean.Expr → Lean.Expr → Lean.Expr
Lean.Expr.lam : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
Lean.Expr.forallE : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
Lean.Expr.letE : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
Lean.Expr.lit : Lean.Literal → Lean.Expr
Lean.Expr.mdata : Lean.MData → Lean.Expr → Lean.Expr
Lean.Expr.proj : Lean.Name → Nat → Lean.Expr → Lean.Expr

These are bound variables, free variables, metavariables, sorts, constants with universe levels, applications, functions, dependent function types, local definitions, numeric and string literals, annotations, and structure projections. The type theory they encode is described in terms, types and judgments. A term handed to the Lean kernel for addition may contain neither metavariables nor free variables: the elaborator must have solved every hole and closed every term.

The requests themselves form a second data type, Lean.Declaration, with seven constructors: an axiom, a definition, a theorem, an opaque constant, a block of mutually recursive definitions, the quotient primitives, and a block of inductive types. What the table stores, Lean.ConstantInfo, has eight: the same kinds, minus the mutual block, plus the constructors and recursors that the Lean kernel itself generates for each inductive type. Both are printed by #print in the same way as Expr above.

What it checks

For every constant, whatever its kind, the Lean kernel checks that the name is not already taken, that no universe parameter is listed twice, that the stated type contains no metavariables or free variables, and that the type is itself well typed with a sort as its type. Then it checks by kind.

An axiom is accepted once its type passes. Nothing else is checked, which is why axioms are listed by #print axioms and why the edition treats them on their own page, the three axioms.

A definition, a theorem or an opaque constant has a value. The Lean kernel infers the value's type and asks whether it is definitionally equal to the stated type. For a theorem it also checks that the stated type is a proposition. In the notation of the foundations pages, a definition $c:T:=v$ is accepted when

$\frac{⊢T:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u⊢v:T^{\prime }{T}^{\prime }\equiv T}{c:T:=v\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{p}\mathrm{t}\mathrm{e}\mathrm{d}}$

where $\equiv$ is definitional equality, the subject of definitional equality. Much of the Lean kernel's work is in that last premise. Its implementation in 4.34.1 tries, in order: quick structural checks; full evaluation when the second term is the Boolean true and the first has no free variables, a path its source comment ties to the decide tactic; reduction to weak head normal form; proof irrelevance; lazy unfolding of definitions, the side with the greater definitional height first; then comparison of arguments, eta for functions, eta for structures, string literals and unit-like types.

A block of mutually recursive definitions is accepted only when it is marked partial or unsafe. Ordinary recursive functions reach the Lean kernel already compiled into recursors, as structural and well-founded recursion explains, so the Lean kernel has no termination checker to trust.

An inductive type is checked hardest, because its constructors and its recursor become axiom-like rules. For each constructor the Lean kernel checks that its type is well typed, that its parameters match the type's parameters, that each field lives in a universe no larger than the type's own (unless the type is a proposition), that the type being defined occurs only strictly positively, and that the constructor returns the type being defined. It then generates the recursor and its computation rules. Inductive types and recursors gives the rules; here is the positivity check refusing a type that would make the logic inconsistent:

inductive Bad where
  | mk : (Bad → Nat) → Bad

error: (kernel) arg #1 of 'Bad.mk' has a non positive occurrence of the datatypes being declared

The prefix (kernel) marks a message that comes from the Lean kernel and not from the elaborator. Some checks are made twice. A constructor field in too large a universe, such as mk : Type → Big for Big : Type, is caught first by the elaborator, which gives a fuller message; the Lean kernel would refuse it too.

What it does not see

The Lean kernel sees no syntax, no notation, no macro, no tactic, no instance search and no coercion. It performs no unification and no termination checking. A proof written with fifty tactic steps and the same proof written as a term reach it as the same kind of object, an Expr, and it cannot tell how either was found. This is the point of the design: the elaborator (elaboration) and the tactic framework may be as clever, as large and as buggy as they like, because what they produce is checked again.

The arrangement can be tested by going around the elaborator. The following metaprogram hands the Lean kernel a theorem whose stated type is False and whose proof is True.intro:

import Lean
open Lean Elab Command

#eval show CommandElabM Unit from do
  let decl := Declaration.thmDecl {
    name := `bogus, levelParams := [], type := mkConst ``False,
    value := mkConst ``True.intro }
  liftCoreM (addDecl decl)

error: (kernel) declaration type mismatch, 'bogus' has type
  True
but it is expected to have type
  False

Computation inside the check

Deciding definitional equality means running programs, so the Lean kernel contains an evaluator. Pure unfolding would make arithmetic on numerals hopeless, since Nat is unary in its definition. The Lean kernel therefore computes Nat.add, Nat.sub, Nat.mul, Nat.div, Nat.mod, Nat.gcd, Nat.pow, Nat.beq, Nat.ble, the bitwise operations and the shifts directly on literals, with the arbitrary-precision numbers of Lean's runtime. Their size is capped all the same: the Lean kernel refuses a natural-number literal, whether written in the source or produced by this arithmetic, that takes more than 128 MB, a default that the operating-system variable LEAN_NAT_MAX_SIZE can change.

theorem big : 2 ^ 64 * 2 ^ 64 = 2 ^ 128 := rfl
#print axioms big

This prints 'big' does not depend on any axioms. The cost is that this arithmetic, and the runtime code behind it, is part of what must be trusted.

Its implementation

The reference manual states that the Lean kernel is written in C++, and that independent reimplementations exist in Rust and in Lean, the aim being to have as many implementations as possible so that they can be cross-checked against each other. In version 4.34.1 the directory src/kernel of the Lean source holds 36 C++ source and header files totalling 8,071 lines, blank lines and comments included; this count was made for this page by running wc -l over those files as they stand at that version. The count is a lower bound on what is trusted, not a measure of it: those files include headers from Lean's runtime and utility libraries, for numbers, names and memory management, which the count leaves out. The largest files are the type checker (1,373 lines) and the checker for inductive types (1,417 lines). The paper that introduced Lean 4 describes the Lean kernel as relatively small.

Lean's environment

Lean's environment, its table of definitions and theorems, is the Lean kernel's state. In 4.34.1 the Lean structure Lean.Kernel.Environment maps each constant's name to its ConstantInfo, and its documentation says that this table contains every constant that has already been type checked by the Lean kernel, that it is never destructively updated, and that its constructor is private to protect against changes that bypass the Lean kernel. The same structure carries extensions, further tables for data the Lean kernel ignores, such as simp lemmas, custom pretty printers and the compiler's intermediate code. Adding a constant returns a new table; nothing already accepted is changed.

Where the trust ends

The checked table is only as good as the path into it. Lean 4.34.1 has an option, debug.skipKernelTC, whose own description warns that setting it "may compromise soundness" because proofs are then not checked by the Lean kernel, and a matching function, addDeclWithoutChecking. A Lean source file can also run arbitrary code while it is processed. The reference manual's guidance on validating proofs therefore recommends replaying the compiled files through the Lean kernel with a separate checker, and, for adversarial settings, building the proofs in a sandbox, exporting them and replaying them with the Lean kernel or an independent checker. Proof export and independent checkers takes this up. The soundness of the type theory itself, which no checker can establish from inside, is the subject of consistency and the metatheory.

Next

Metavariables and unification describes the holes the elaborator must fill before a term may reach the Lean kernel.