Lean theorem prover/Explainers/Programs and proofs in one language

Technical version: The compiler and runtime· Monads and do-notation· Syntax extension and hygienic macros

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 programming language as well as a proof checker. A definition written in Lean can be run as a program and reasoned about in a theorem, and it is written once for both. This page shows that, says how Lean turns definitions into programs, marks the places where running and proving part company, and says how the project this wiki records relies on the property.

One definition, two uses

Here is a definition of the sum of the numbers from 1 to n, a command that runs it, and a theorem about it:

def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => sumTo n + (n + 1)

#eval sumTo 100

theorem sumTo_formula (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih => grind [sumTo]

Lean 4.34.1 prints 5050 and accepts the theorem. The two uses answer different questions. Running the definition gives the answer for one number at a time; however many numbers are tried, some remain untried. The theorem covers every natural number at once, by induction (see induction, as the machine sees it). Because both rest on the same definition, there is no second copy that could drift from the first: the program that is run is the object the theorem is about.

From definition to program

Lean runs definitions in one of two ways. An interpreter can run them directly. Or Lean can compile them: Lean's compiler translates them into C, one C file for each Lean source file, and a C compiler that ships with Lean turns that into native code for the machine. The paper that introduced Lean 4 describes it as an efficient functional programming language, and names one reason efficiency matters: people write their own proof automation in Lean, and that automation has to be fast.

Lean 4 is itself largely a Lean program. The same paper describes it as a reimplementation of the Lean theorem prover in Lean, in which users can extend the parser, the elaborator, the tactics and the code generator from Lean. The Lean kernel is the exception: it is written in C++. So the tools that help a person write proofs are Lean programs, while the part that judges them is kept separate (see the small trusted core).

There is a free book on using Lean as a programming language, Functional Programming in Lean; the code in its current edition was tested with Lean 4.33.0.

Programs that act on the world

A program has to read input and print output. A proof does neither. Lean keeps the two apart by type: an action such as printing a line has a type of its own, IO, and a sequence of actions is written in a block that begins with do (see monads and do-notation). Continuing the same file:

def main : IO Unit := do
  for n in [10, 100, 1000] do
    IO.println s!"the sum up to {n} is {sumTo n}"

#eval main

Lean prints:

the sum up to 10 is 55
the sum up to 100 is 5050
the sum up to 1000 is 500500

The action main uses sumTo, and the theorem above is about that same function; to believe it of the values printed is also to trust the compiler that turned sumTo into a program. The part that talks to the world is thin; the part that computes is the part that is proved.

Where running and proving part

Programs that may never stop. Lean's logic needs every function to give an answer, so a definition that calls itself has to be shown to finish (see functions that always finish). A program does not always come with such a proof. Here is one for which nobody has one: starting from a number, halve it if it is even, otherwise triple it and add one, and count the steps until it reaches 1. Whether this ends for every starting number is a famous open question, the Collatz problem. Lean accepts the program if it is marked partial:

partial def collatz (n : Nat) (steps : Nat := 0) : Nat :=
  if n ≤ 1 then steps
  else if n % 2 == 0 then collatz (n / 2) (steps + 1)
  else collatz (3 * n + 1) (steps + 1)

#eval collatz 27

It runs, and prints 111. But the program says nothing to the logic. Lean's reference states that the Lean kernel treats a function marked partial as an opaque constant, which it neither unfolds nor computes with; all that soundness requires is that its result type has at least one value. Even the plainest fact about it cannot be proved by looking inside:

example : collatz 1 = 0 := by
  unfold collatz
  rfl

Lean refuses, with the message "Tactic `unfold` failed to unfold `collatz` in", followed by the goal collatz 1 = 0.

Programs run in place of definitions. Lean lets a library say that, when a definition is run, another function should be run instead, usually a faster one. The theorems are about the definition; the program runs the replacement. If the two disagree, the program and the proofs no longer describe the same thing. What has to be trusted shows this happening, and what it costs when a proof relies on the compiled program.

New notation. Lean's syntax can be extended from Lean, through a system of macros designed so that names introduced by a macro cannot collide with names in the surrounding text. This serves programmers and mathematicians alike, and it is one more thing a reader has to know when reading a statement (see stating the right thing).

The project this wiki records

Principia Machina depends on this property. Its earlier version kept its rules in prose and computed them in two hand-written copies, one for the wiki's server and one for the agents that do research, held in agreement by a large set of test cases. The new version writes the rules once, as Lean definitions and theorems, and compiles the same sources into one program, the Calculator, which is to compute every value the specification defines, on the server and beside each agent. As of 14 October 2026 a first Calculator exists. A test has shown that a compiled Lean program runs on the wiki's server when started as a command, though not inside a web request, so the server's gatekeeper, Custos, is to call the Calculator outside the web request. These are the project's own statements, on the move to Lean; Principia Machina describes the project in this edition.

Next

A library of mathematics describes Mathlib and the libraries that come with Lean.