Consistency and the metatheory

Plain-language version: What has to be trusted

The metatheory of Lean is what can be proved about its type theory rather than in it. The central question is consistency: whether a closed proof of False can ever pass Lean's kernel. The answer known today is relative, and it was proved for the type theory of Lean 3. That theory, with its three axioms, can be interpreted in Zermelo–Fraenkel set theory with choice (ZFC) extended by inaccessible cardinals, one axiom "there are $n$ inaccessible cardinals" for each natural number $n$, so it is consistent if that set theory is. Several properties one might expect of a type theory fail for Lean, among them decidability of definitional equality and normalisation, and none of these failures makes the checker unsound. If Lean is consistent, it cannot prove its own consistency. This page sets out each of these points and its source.

The consistency theorem

Carneiro's thesis of 2019 writes down the type theory of Lean 3 in full, including the three axioms, and constructs a set-theoretic model of it. Its conclusion, Corollary 6.8, is that Lean is consistent if ZFC together with the axioms "there are $n$ inaccessible cardinals", for every natural number $n$, is consistent: there is no proof of False that the Lean kernel verifies.

$\mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{Z}\mathrm{F}\mathrm{C}+\{\mathrm{\exists }n\text{ inaccessible cardinals}:n<\omega \})\Rightarrow \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{L}\mathrm{e}\mathrm{a}\mathrm{n})$

The model is the expected one. Types are sets and terms are their elements. Prop is a two-element set whose members are the empty set and a one-element set, so every proposition is interpreted as empty or as a one-element set, which validates proof irrelevance. Each higher universe is interpreted inside a level of the cumulative hierarchy cut off at an inaccessible cardinal, because universes are closed under function types and inductive types, which makes them Grothendieck universes. Lean has a universe for every natural number, so the full hierarchy calls for an inaccessible for each of them; a single proof mentions only finitely many universes, which is why the hypothesis is stated one $n$ at a time. The impredicativity of Prop corresponds to full power sets in ZFC.

Carneiro calls the assumption optimal, for the following reason. Inside Lean one can build a model of ZFC in each universe above the lowest, and define inaccessible cardinals in the larger ones, so Lean proves the consistency of ZFC with any given finite number of inaccessibles.

Relative consistency and Werner's theorem

The two directions were matched for the Calculus of Inductive Constructions, the theory behind Coq, by Werner in 1997. Writing ${\mathrm{Z}\mathrm{F}\mathrm{C}}_n$ for ZFC with $n$ inaccessibles and ${\mathrm{C}\mathrm{I}\mathrm{C}}_n$ for the calculus with $n$ universes, Carneiro summarises Werner's result as

${\mathrm{Z}\mathrm{F}\mathrm{C}}_n⊢\mathrm{C}\mathrm{o}\mathrm{n}({\mathrm{C}\mathrm{I}\mathrm{C}}_{n+1}){\mathrm{C}\mathrm{I}\mathrm{C}}_{n+2}⊢\mathrm{C}\mathrm{o}\mathrm{n}({\mathrm{Z}\mathrm{F}\mathrm{C}}_n)$

so that the unions over all $n$ are equiconsistent. Werner's encoding of set theory in the calculus also assumes excluded middle and a type-theoretic axiom of choice. Werner's construction of set theory inside type theory has been replicated in Lean with minor changes, which gives ${\mathrm{L}\mathrm{e}\mathrm{a}\mathrm{n}}_{n+2}⊢\mathrm{C}\mathrm{o}\mathrm{n}({\mathrm{Z}\mathrm{F}\mathrm{C}}_n)$. Carneiro's model supplies the other direction, ${\mathrm{Z}\mathrm{F}\mathrm{C}}_{n+1}⊢\mathrm{C}\mathrm{o}\mathrm{n}({\mathrm{L}\mathrm{e}\mathrm{a}\mathrm{n}}_{n+1})$, so Lean with all its universes is equiconsistent with both. He does not attempt sharp universe bounds, and notes that matching Werner's exactly would require global choice, a choice function on the whole set-theoretic universe, to interpret Lean's choice axiom. Lean's consistency strength is thus that of the union of the theories ${\mathrm{Z}\mathrm{F}\mathrm{C}}_n$.

What fails

The same thesis records negative results, and later work adds one more.

Definitional equality is undecidable, and so is type checking. The accessibility predicate, together with proof irrelevance, lets a definitional-equality question encode the halting problem. The argument is on proof irrelevance and subsingleton elimination.

The checker's equality is weaker than the theory's. Lean's kernel implements a decidable approximation, algorithmic equality, which is not transitive. Typing measured by it fails subject reduction, and the reduction relation is not confluent (the Church–Rosser property fails), so reducing both sides to normal form is not a decision procedure. A modified reduction restores confluence at the cost of termination, enough to prove that every term has a unique type up to definitional equality.

Normalisation fails. Abel and Coquand showed that a type theory with an impredicative Prop and a proof-irrelevant equality loses normalisation. One of their counterexamples uses only propext, one of Lean's standard axioms, and gives a closed proof with no weak head normal form; they note that it replays directly in Lean 3.4.2. It transcribes directly into Lean 4.34.1:

set_option linter.defProp false

def T : Prop := ∀ A : Prop, A → A

def delta : T → T := fun z => z (T → T) id z

def omega : T := fun A a => cast (propext ⟨fun _ => a, fun _ => id⟩ : (T → T) = A) delta

def Omega : T := delta omega

#print axioms Omega

This prints 'Omega' depends on axioms: [propext]. The type T quantifies over all propositions, which is possible only because Prop is impredicative. Given any proposition A and a proof a of it, propext makes T → T equal to A, because both are true; omega casts delta along that equation. When the cast is used at A = T → T itself the two sides of the equation coincide, the cast reduces away, and delta omega unfolds back to delta omega. Asked to normalise the proof, Lean gives up, even with its recursion limit raised to 20,000:

set_option maxRecDepth 20000 in
#reduce (proofs := true) Omega

The error is maximum recursion depth has been reached. The failure reaches beyond proofs. Carneiro's later paper on an independent checker gives a variant in which a natural number defined by eliminating a proof built from Omega sends a definitional-equality check into the same loop:

inductive Foo : Prop
  | mk : T → Foo

def foo : Foo := Omega Foo (Foo.mk fun _ => id)

example : foo.recOn (motive := fun _ => Nat) (fun _ => 1) = 1 := by
  rfl

Lean again reports maximum recursion depth has been reached. Abel and Coquand stress what is not at stake: consistency and canonicity are unaffected, and they compare the situation to extensional type theory, which has an equality reflection rule.

Why the checker is still sound

Carneiro's argument needs one thing: whatever the checker accepts must be derivable in a theory that has a model. He proves that algorithmic equality implies the ideal definitional equality for well-typed terms. So if a term of type False passed the algorithmic typing judgment, his description of what Lean's kernel checks, that term would have type False in the ideal system, and the model would then contain an element of the empty set. This is precisely the proof of Corollary 6.8.

The failures above are therefore failures of completeness and of termination, not of soundness. A checker that is incomplete rejects some correct terms. A checker that may not terminate either loops or, as Lean does in the examples above, stops at a resource limit and reports an error. Neither outcome accepts a false statement. Carneiro observes that the soundness proof of his thesis, unlike MetaRocq's, does not depend on termination.

Proving consistency inside Lean

Gödel's second incompleteness theorem sets the limit. A consistent formal system in which a modest amount of arithmetic can be carried out cannot prove its own consistency. Lean formalises far more than that arithmetic, so if Lean is consistent, no Lean proof of "Lean is consistent" exists. Carneiro's theorem respects the limit in the usual way: it is a proof in a different system, ZFC with inaccessibles, and its conclusion is relative to that system's consistency. The independent-checker project names Gödel's theorem as the reason that nothing implying the unconditional soundness of Lean will be directly provable in Lean, and plans to formalise Carneiro's relative consistency proof, which assumes large cardinals.

The theory and the implementation

A consistency proof covers a mathematical description of the theory, not the program that checks it. The Lean 4 kernel extended the theory Carneiro analysed with features such as nested inductive types and η for structures. Carneiro writes that these change the theory enough that the 2019 proof no longer applies directly, pointing to later work that covers some of the changes, and that some soundness bugs entered Lean's kernel during the move to Lean 4. One response is independent checking: a second complete type checker written in Lean, able to check all of Mathlib, with part of it formally verified against a formalisation of the type theory. That work has already found and reported one soundness bug in Lean's kernel, since fixed. The reference manual's guide to validating proofs lists the soundness of Lean's logic among the assumptions that remain even after the strictest checks. The checkers themselves are the subject of proof export and independent checkers.

Next

Elaboration begins the pages on how Lean works, from the text a person types to the term the Lean kernel checks. The Lean kernel describes the program whose soundness this page has been about.