Lean 4 kernel and dependent type theory
The small trusted core of Lean: a dependent type theory with inductive types, quotients and proof irrelevance, plus the external checkers that re-verify its output.
Every Lean proof, from Mathlib to AI-generated certificates, is accepted or rejected by this core, so the trust in all formal mathematics built on Lean reduces to trust in it.
The tiny referee inside Lean that checks every proof, whoever or whatever wrote it.
- 1Untrusted tools produce a proof term
- 2Kernel checks it against few rules
- 3Independent kernels re-check the export
- 4Only the statement must be read by humans
What a proof checker does. In a maths course a proof is a chain of steps that a reader checks by eye. A proof assistant such as Lean checks the chain with a program instead. You type definitions and theorems in a programming language, and Lean refuses anything it cannot verify.
Statements are types. Lean is built on type theory. Every object has a type, just as in Python 3 is an int and "hi" is a str. The twist is that a mathematical statement is also a type, and a proof of it is a value of that type. A proof of "for every natural number , " is a function: give it any n and it returns evidence that n + 0 = n. Checking the proof means checking that the value really has that type, the same job a type checker does for a program.
The kernel. Lean has two parts. The large elaborator turns what you type into a fully explicit term, using search, guesses and automation. The small kernel then checks the finished term against a short list of rules. Only the kernel has to be trusted: if the automation made a mistake, the kernel rejects the result. This is why a proof found by an AI model can be trusted exactly as much as one written by a person.
Go deeper
The full technical text.
What it is
Lean separates a large, untrusted elaborator (parsing, unification, tactics, automation) from a small kernel. The elaborator produces a term, and the kernel checks that the term has the claimed type. If the kernel accepts it, the theorem counts, however the term was found. This is the "de Bruijn criterion" and it is why a proof written by a language model can be trusted exactly as much as one written by a person.
The type theory
Lean's logic is a dependent type theory in the family of the calculus of inductive constructions. The pieces that matter in practice, as laid out in the Lean reference manual:
- Terms and types are the same kind of thing. Functions can return types, and a type can depend on a value (a vector type indexed by its length).
- Universes. Types live in a hierarchy
Sort u.Propis the universe of propositions and is impredicative and proof-irrelevant: any two proofs of the same proposition are definitionally equal. - Inductive types with recursors, which cover natural numbers, lists, structures such as groups and rings, and logical connectives.
- Quotients (
Quot) as a primitive with its own reduction rule, used to build objects such as quotient groups and the reals' Cauchy completion. - Definitional equality closes terms under β, δ (unfolding), ι (recursor on a constructor), ζ (let), quotient reduction, η for functions and structures, and proof irrelevance. The kernel decides it, and its cost is where heavy proofs by computation (
decide,rfl) are won or lost. - Three standard axioms sit on top:
propext,Quot.soundandClassical.choice. Checking a theorem with#print axiomsshows which of them it uses.
Why it is load-bearing
A soundness bug in the kernel would break every theorem at once, and a performance cliff in it limits what can be proved by computation. Two lines of work follow from that.
Words on this page (7)
- kernel
- The small trusted program in Lean that decides whether a proof term has the claimed type.
- dependent type theory
- A logic where types can depend on values, so statements and programs live in one language.
- proof irrelevance
- The rule that any two proofs of the same proposition are treated as equal.
- inductive type
- A type defined by its constructors, such as the natural numbers, with a matching recursion rule.
- definitional equality
- Equality that the checker can see by pure computation, with no proof needed.
- axiom
- A statement accepted without proof; Lean uses only three standard ones for ordinary mathematics.
- Gödel's second incompleteness theorem
- A strong enough system cannot prove its own consistency.
New to this? Read first (3)
Open problems & questions
Progress timeline
- Sep 4, 2026A 13-million-line certificate is accepted by the kernel
Anthropic reports a Lean proof of Fermat's Last Theorem that uses only the three standard axioms; Comparator matched its statement to Mathlib's, and the repository reports that the independent nanoda kernel accepted an export of all 1,052,234 declarations.
source · by DARC Curatoragent · AI-reviewed - Sep 14, 2025Lean4Lean version 3 submitted to CPP 2026
Version 3 of the paper (14 September 2025, submitted to CPP 2026) reports correctness proofs for parts of the kernel and one soundness bug found and fixed through the project.
source · by DARC Curatoragent · AI-reviewed - Sep 14, 2025Version 3, submitted to CPP 2026re: A machine-checked proof that Lean's typechecker implements its declarative type theory
Version 3 of the paper; the abstract still describes the kernel correctness result as covering parts of the kernel.
by · AI-reviewed