Lean theorem prover

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 proof assistant and a programming language. A person writes definitions, statements and proofs in Lean's formal language, and Lean checks each proof against the rules of its logic before it accepts the statement as a theorem. The same language is used to write programs that run, and a definition used by a program can also be the subject of a theorem.

Lean was begun in 2013 by Leonardo de Moura at Microsoft Research. Its fourth version, Lean 4, is written largely in Lean itself. Since 2023 it has been developed by the Lean Focused Research Organization, a non-profit, with a new version about every month, and its users maintain Mathlib, a library of mathematics checked by Lean.

This edition describes Lean: what it checks and how, the type theory behind it, how the program is built, where it came from, and what it is used for. It is written for two readers at once: one with no logic or programming who wants to know what a checked proof is, and one who wants the rules. Its Lean code was checked with Lean 4.34.1, and its statements about the state of things are dated October 2026.

What Lean checks

In Lean a statement is a type, and a proof of it is a term of that type: an expression built by the rules of the logic. Checking a proof is then checking that a term has the type claimed for it, the operation a compiler performs on a program. This is the idea called propositions as types. The logic is a dependent type theory, in which a type may depend on a value. It belongs to the family of the Calculus of Inductive Constructions: propositions form a universe of their own, and almost every type, from the natural numbers to equality, is built from a few constructors.

One part of Lean makes the check: the Lean kernel, a small type checker written in C++. Everything else, the parser, the elaborator that fills in what a person leaves out, the tactics that construct a proof step by step, the automation that searches for one, only proposes terms, and the Lean kernel accepts or refuses each of them. A fault in a tactic can stop a proof from being found, but a wrong term it produces is refused. Code that goes around the Lean kernel on purpose is a separate matter, taken up at Proof export and independent checkers.

A theorem Lean accepts follows, as written, from the rules of Lean's logic and from the axioms its proof uses. Lean provides three axioms, propositional extensionality, the soundness of quotients and a principle of choice, and it lists on request the axioms any theorem depends on. The rest of what an accepted proof rests on is a short list: that the Lean kernel is correct, that the logic is consistent, and that the machine runs the Lean kernel faithfully. The consistency of the logic is known relative to set theory with inaccessible cardinals, and was proved for the type theory of Lean 3. What has to be trusted gives the list in full.

The check does not establish two things. It does not establish that a statement says what its author meant: a theorem with a mistyped hypothesis can be true and say nothing (Stating the right thing). And a theorem about a model of the world is a theorem about the model; whether the world fits the model is a question for experiment (Lean and physics).

Where Lean came from, and what it is used for

Lean draws on fifty years of work. Automath, designed by N. G. de Bruijn from the late 1960s, was the first working system for checking mathematics by computer. Robin Milner's LCF, begun at Stanford in 1972 and redesigned at Edinburgh, introduced tactics. Per Martin-Löf made propositions as types the foundation of a theory of mathematics, and the Calculus of Constructions of Thierry Coquand and Gérard Huet began the family of theories to which Lean's logic belongs. Lean's own history runs from its first versions to Lean 4, whose first stable version appeared in September 2023.

Lean is used to formalise research mathematics, in one case within a month of a proof's appearance; to verify software in industry; to teach proof; to check proofs written by machine-learning systems; and, so far on a small scale, for physics. The Applications pages describe each use together with what it did not establish.

What this edition is not

It is not a tutorial. It does not teach how to write Lean; a reader who wants to learn will find the free books on Further reading more useful.

It is not Lean's documentation. The authority on Lean is its documentation, chiefly The Lean Language Reference, which describes itself as a reference work rather than a tutorial, and its source code. The pages here cite both. Every block of Lean code on them was compiled with Lean 4.34.1, without Mathlib unless a page says otherwise, and every message quoted is the one that version prints, so a reader can run the code and see.

Three levels of reading

The three levels of the edition. Solid arrows follow the reading order that each page's Next section continues; dashed lines join each explainer to the technical pages named at the head of both.

The edition is written at three levels.

1. This page: what Lean is and what it checks, and a map of the rest.
2. The explainers: twenty-two pages in plain language, for a reader with no logic or programming. They use no notation beyond a short line of Lean where one shows the point better than words.
3. The technical pages, in two sections. The twelve Foundations pages set out the type theory, with its rules written as formulas and Lean code that compiles. The twelve System pages describe how Lean works, from elaboration to the compiler, with Lean's own output.

Each explainer but the last, on physics, is paired with the technical pages that treat its subject in full, and the pairing is shown at the head of both: an explainer carries a line headed Technical version, a technical page a line headed Plain-language version. A reader can enter at either level and cross at any point. The History and Applications pages sit beside the explainers and are written at their level. Six reference pages close the edition.

How to read it. Every page ends with a section headed Next, whose first link continues one reading order: this page, the explainers, the Foundations pages, the System pages, the History, the Applications, and the reference pages; a second link, where there is one, leads sideways. A reader who wants the idea without the formalism can read the explainers, the History and the Applications. A reader who knows some logic can start at Terms, types and judgments and use the explainers as summaries. Notation sets the formulas of the Foundations pages beside Lean's own syntax for the same things, and the Glossary defines the terms.

The pages

Explainers

Explainer	Technical pages
What a proof assistant does	Elaboration, The Lean kernel
Checking instead of convincing	Terms, types and judgments, The Lean kernel
Propositions as types	Terms, types and judgments, Dependent function types
Types as specifications	Dependent function types, Inductive types and recursors
Why there is no type of all types	Universes and Prop
What the axioms are	The three axioms, Classical logic from choice, Quotient types
Two kinds of equality	Definitional equality, Propositional equality, Proof irrelevance and subsingleton elimination
Functions that always finish	Structural and well-founded recursion
Building things from constructors	Inductive types and recursors
Induction, as the machine sees it	Inductive types and recursors, Structural and well-founded recursion
Tactics	The tactic framework, Metaprogramming in Lean
Holes and goals	Metavariables and unification, The tactic framework
Automation and its limits	Decision procedures
When Lean says no	Elaboration, Metavariables and unification
Computation inside proofs	Definitional equality, Decision procedures
The small trusted core	The Lean kernel
What has to be trusted	The Lean kernel, Consistency and the metatheory
Checking a proof again later	Proof export and independent checkers
Stating the right thing	Terms, types and judgments
Programs and proofs in one language	The compiler and runtime, Monads and do-notation, Syntax extension and hygienic macros
A library of mathematics	Type classes and instance resolution, Lake and Lean projects
Lean and physics	none; it leads to Physics in Lean and Principia Machina

Foundations

• Terms, types and judgments: the typing judgment, contexts, and the small term language the Lean kernel receives.
• Dependent function types: the one function type, of which implication and "for all" are cases.
• Universes and Prop: the hierarchy of types of types, and the universe of propositions.
• Inductive types and recursors: types given by constructors, and the recursor derived from them.
• Structural and well-founded recursion: how recursive definitions reach the Lean kernel, and why they terminate.
• Definitional equality: equality by computation, its rules and its limits.
• Propositional equality: equality as a proposition, and what follows from its single constructor.
• Quotient types: types made by identifying related elements.
• The three axioms: what each says, and how a theorem's dependence on them is audited.
• Classical logic from choice: excluded middle as a theorem.
• Proof irrelevance and subsingleton elimination: why the content of a proof never matters, and what that costs.
• Consistency and the metatheory: what is known about Lean's consistency.

System

• Elaboration: from typed text to a fully explicit term.
• The Lean kernel: what the checker checks, and where its trust ends.
• Metavariables and unification: holes in terms, and how Lean fills them.
• Type classes and instance resolution: values Lean finds by itself.
• The tactic framework: goals, the tactic monad, and a tactic in three lines.
• Decision procedures: five automatic tactics, and what each asks to be trusted.
• Syntax extension and hygienic macros: new notation, and names that cannot be captured.
• Metaprogramming in Lean: programs whose data is Lean itself.
• The compiler and runtime: from a definition to machine code.
• Lake and Lean projects: Lake, Lean's tool for compiling projects, and how a project fixes its version of Lean.
• Proof export and independent checkers: checking a proof again, with other programs.
• Monads and do-notation: effects as values in a pure language.

History

• Automath: the first system for checking mathematics by computer.
• LCF and the tactic idea: protected theorems and programmable tactics.
• Martin-Löf type theory: propositions as types made a foundation.
• The Calculus of Constructions: Coquand and Huet's theory, Coq, and Lean's place in the family.
• Lean 1 to Lean 3: the first versions, from 2013.
• Lean 4: the rewrite in Lean, and the move of the mathematical library.
• Mathlib and its community: the library, its review and its size.
• The Liquid Tensor Experiment: a challenge from research mathematics, 2020 to 2022.
• Lean since 2023: a version every month, new automation, and two flaws found in the Lean kernel.

Applications

• Research mathematics: formalised results, and why mathematicians formalise.
• The polynomial Freiman-Ruzsa conjecture: a new theorem checked in three weeks.
• The Fermat's Last Theorem project: a funded project, and a machine-written proof.
• The equational theories project: twenty-two million implications, with Lean as referee.
• Software verification: three industrial uses, and what "verified" covers in each.
• Teaching with Lean: a game, textbooks and courses.
• Machine learning and theorem proving: Lean as the checker of machine-written proofs.
• Physics in Lean: a library for physics, and what a theorem about a model says.
• Principia Machina: this wiki's framework for testing physical hypotheses, restated in Lean.

Reference pages

• Chronology: dated events, from Automath to October 2026.
• Glossary: the edition's terms, defined.
• Notation: the formulas beside Lean's syntax.
• Sources: what was read for the edition, and what was not.
• Bibliography: the works the edition cites.
• Further reading: books, a game and papers for a reader who wants more.

Next

What a proof assistant does, the first explainer. A reader who wants the rules first can begin at Terms, types and judgments.