How Lean works — where it came from, and how checking works

The idea is the confluence of two threads that started far apart.

The first thread: a proof can be written as an object a machine can handle. The mechanism that assigns types to functions and the mechanism that proves an implication "if A then B" have the same shape, a correspondence known as the Curry–Howard correspondence. One half of the name comes from Curry's 1934 paper "Functionality in Combinatory Logic". With this correspondence, a proof is no longer something you read and find convincing; it is a concrete piece of writing, a term of the right type.

The second thread: the part that checks should be small. In 1972, Milner implemented a proof checker called LCF at Stanford. In the LCF tradition, the tools that assemble a proof (tactics) can be written freely in a metalanguage, while whether the finished product is accepted is decided by a small core alone. No matter how many tools are added, the part you have to trust does not grow.

The first serious meeting of the two threads was de Bruijn's Automath. Designed as a language for writing down mathematical proofs and having a machine check them, it was reported in 1970. It was the first full-scale attempt to put mathematical proofs through machine checking. In the 1970s, Jutting checked Landau's Grundlagen der Analysis in this language.

The design principle that emerged from this is what later came to be called the de Bruijn criterion: keep the proof not as an intermediate state of the check but as a self-contained term, so that a small, independent checker can read it again. In the classic comparison table of proof assistants, this stands as its own item, "small proof kernel (has proof objects)". Lean's official documentation says the same thing: "a proof term is sufficient evidence of the truth of a theorem, and it can be subjected to independent verification".

On the type-theory side, Martin-Löf's intuitionistic type theory (1975) set out to rebuild the foundations of mathematics on top of types, and building on it, Coquand presented the first version of the Calculus of Constructions in 1985. The first implementation was begun in 1984 by Huet and Coquand, and its core was a type checker called the Constructive Engine. In 1989, Coquand and Paulin added inductive definitions, giving the Calculus of Inductive Constructions. This is the logic of Coq, and it is also the foundation of Lean's logic.

The large theorems actually checked in this lineage are mixed into the timeline below.

Lean sits at the continuation of this table. Its underlying type theory is of the same family as Coq's, and its design principle inherits the "small core" of the LCF tradition.

Lean was started in 2013 by de Moura at Microsoft Research. The first commit is from July of that year. Since then, both the notation and the implementation have been replaced several times over.

The first public release was 0.1 (2014). Version 0.2 had a homotopy type theory mode alongside the standard logic, and is frozen in a separate repository under the name Lean 2. Lean 3 (January 2017) brought a wider user base, and in July of the same year the mathematics library mathlib was created. Development of Lean 4 began in April 2018, and the official release came in September 2023.

One of the distinguishing features of Lean 4 is that it is rewritten in Lean itself. The parser, the elaborator, and the tactics are all written in Lean, and users can extend them in Lean as well. Parts that in earlier versions could only be added by writing C++ can now be written in the same language as the library.

mathlib, for its part, grew as the work of a community rather than of an individual. Its design is recorded in a 2019 paper, and it has now passed a million lines. The port from Lean 3 to Lean 4 was completed in July 2023.

In that same July 2023, the way Lean itself is developed changed. de Moura and Ullrich founded Lean FRO (a Focused Research Organization), and Lean became a tool developed under a non-profit organization.

Two formalizations in Lean stand as landmarks of scale. The Liquid Tensor Experiment was posed in December 2020 as a challenge, "can this theorem be formalized?"; the proof of the first target was announced on 28 May 2021, and the whole was completed on 14 July 2022. For the polynomial Freiman–Ruzsa conjecture, a formalization project was launched right after the proof paper appeared in November 2023, and its first stage is complete.

Between the string a user types and its acceptance as a theorem, Lean passes through the following stages.

What does the work here is that the core type theory is far simpler than the language users write in. In the words of the official documentation, "this core theory is much simpler, which allows the trusted kernel to be kept very small". However clever the elaborator becomes, what the kernel reads is still the simple language.

The compiler is not in the line of verification. It is a separate track for producing runnable programs and has no bearing on whether a theorem is correct. The exception is native_decide: only then does a result produced by the compiler enter the logic as an axiom (01).

For the core type theory, we note just the names.

One distinction, to close. mathlib is not part of the kernel. It is a library, that is, a collection of definitions and theorems written in Lean, and in status it is the same as the files a user writes. If a wrong proof got into mathlib, it would still have gone through the kernel; and conversely, remove all of mathlib and the kernel works exactly as before.

This is the heart of the page. So that you can follow it without ever having touched Lean, we start with an analogy and then look at the real thing one step at a time.

The counter-clerk analogy

Think of a proof as a completed form. The proposition is the form's layout, and the proof is one sheet with that layout filled in.

The kernel is a clerk at a counter who knows only the rules for filling in the form. The clerk does not look at whose hand wrote it, whether it is handwritten or printed, or how many drafts were thrown away. All the clerk looks at is whether the fields of the form are filled in according to the rules. Filled in, it is accepted; not filled in, it is handed back.

This "not looking" is the point. The tools that assemble the proof (tactics), the search programs, human intuition: all of these are outside the counter. What the clerk looks at is only the one sheet finally submitted.

Step one — closing by computation

We look at the smallest form there is.

theorem two_add_two : 2 + 2 = 4 := rfl

After the : is the layout (the proposition); after the := is the filled-in part (the proof). rfl is a one-word entry meaning "both sides compute to the same thing", and the kernel that receives it actually computes both sides.

The rules of computation are the definition of addition on the natural numbers itself. This is how it is in Lean.

#check @Nat.add_zero
#check @Nat.add_succ

Nat.add_zero : ∀ (n : ℕ), n + 0 = n
Nat.add_succ : ∀ (n m : ℕ), n + m.succ = (n + m).succ

"Adding 0 to something gives that thing" and "adding 'the successor of something' gives the successor of the sum". That is all there is: two rules. succ is the operation that makes "the next number", and the right-hand 2 in 2 + 2 is the successor of the successor of 0. So the kernel needs only three moves.

example : 2 + 2 = Nat.succ (2 + 1) := rfl
example : 2 + 1 = Nat.succ (2 + 0) := rfl
example : 2 + 0 = 2 := rfl
example : Nat.succ (Nat.succ 2) = 4 := rfl

All four lines pass the check. The first and second lines are Nat.add_succ, the third is Nat.add_zero, and the fourth is the fact that the notation 4 denotes the successor of the successor of 2. Chain these four together and you get from 2 + 2 to 4. What the kernel does for the theorem at the top is exactly this.

Step two — a proof of "and" is a pair

Propositions that do not close by computation fit the same frame. We look at the layout of "A and B".

#check @And.intro

@And.intro : ∀ {a b : Prop}, a → b → a ∧ b

Read it as: "for propositions a and b, given a proof of a and a proof of b, you get a proof of a ∧ b". In other words, a proof of a ∧ b is a pair of a proof of a and a proof of b.

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

(hp : p) declares "receive a proof of p under the name hp", and ⟨ ⟩ is the notation for making a pair. Put the wrong thing in one slot and the clerk hands it back with a reason.

example (p q : Prop) (hp : p) : p ∧ q := ⟨hp, hp⟩

error: Application type mismatch: The last
  hp
argument has type
  p
but is expected to have type
  q
in the application
  ⟨hp, hp⟩

"The second field should hold a proof of q, but a proof of p is in it." It is a note about a defect in the form. The same goes for the rfl side.

example : 2 + 2 = 5 := rfl

error: Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

Strictly speaking, these two notes come not from the kernel but from the elaborator. The elaborator also watches the types itself as it assembles the term, so defects are usually caught before they reach the kernel. The kernel is the final gate that runs the finished term through the same rules once more.

Step three — a proof of "implies" is a function

The entry for "if A then B" is a function that takes a proof of A and returns a proof of B.

example (p : Prop) : p → p := fun hp => hp

example (p q : Prop) (h : p → q) (hp : p) : q := h hp

The first line is "p implies p", a function that returns whatever it receives. The second line says that given a proof h of "p implies q" and a proof hp of p, you obtain a proof of q, written as h hp (applying the function to the argument). A step of logic has the same shape as a function call. This is the Curry–Howard correspondence, felt by hand.

Step four — even written with tactics, it ends up as a term

Real proofs cannot be written this briefly. So you line up tactics after by and have them assemble the term for you.

theorem and_swap (p q : Prop) (h : p ∧ q) : q ∧ p := by
  constructor
  · exact h.2
  · exact h.1

constructor is the tactic that splits the goal in two, "to make q ∧ p you need q and p"; exact is the tactic that puts what you have in hand into that field. The assembled result can be seen with #print.

#print and_swap

theorem and_swap : ∀ (p q : Prop), p ∧ q → q ∧ p :=
fun p q h => ⟨h.right, h.left⟩

The four lines of tactics are gone, and a one-line term remains. And its contents are exactly the shapes seen in steps two and three: a function that receives arguments (fun) and a pair of two proofs (⟨ ⟩). Tactics are a tool for writing this term, and this one line is all the kernel receives.

Why it can be believed

With all this in place, what has to be trusted and what does not fall apart cleanly.

Even so, "the kernel's implementation" remains. So there are means for re-reading a finished proof. Lean's official documentation lists ways of confirming, in order of strength.

The third, leanchecker, is a tool that runs Lean's own kernel once more, so it cannot catch defects in the kernel itself. What it catches are defects in the surrounding code that handles the kernel's state, and things of the kind where a metaprogram bypasses the check and adds a declaration.

The fourth is the strongest form currently available. The proof is built in an isolated environment, the proof terms are exported, and outside of it, that is, somewhere the proof-side programs cannot reach, they are run through both Lean's kernel and a separately written, independent checker. The external checker the official documentation names is one implemented independently in Rust, and a venue has been set up for lining up further checkers and comparing them. This is the dividend that the de Bruijn criterion actually pays. Because the proof remains as a term, a different checker can read it again.

Assumptions still remain. The official documentation lists those too: that Lean's logic itself is sound, that the plumbing for export and matching is correct, that the isolated environment is not breached, that there is no defect affecting all the checkers used at once, and that the statement contains no human error or misleading formulation.

Where it can still go wrong

Who guarantees what

What machine checking moved is the boundary between what is confirmed and the means of confirming it. "Is the proof correct?" can be handed to the machine. "Is this theorem what was meant?" cannot. That the latter remains is not a weakness; it is the job that came to the fore once the former was taken care of.

References and sources

The basics of Lean are in 01 What Lean is; running it on your own machine is in 02 Getting started; the meaning of the terms is in 12 Glossary.