What a proof assistant does

Technical version: Elaboration· The Lean kernel

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

A proof assistant is a program that checks proofs written in a formal language, step by step, while a person writes them. Lean is one. This page says what such a program does, how it differs from a program that looks for proofs on its own, which other systems do the same work, and what it means, and does not mean, when a proof assistant says that a proof is checked.

A language with no gaps

A proof in a journal is written for a reader. It skips steps the reader can be trusted to fill in, and it relies on conventions the reader already shares. That is efficient, and it is also where mistakes hide: a step that looks routine may not be.

A proof assistant has no shared conventions to fall back on. Everything is written in a formal language, a notation with fixed rules for what counts as a statement and what counts as a valid step. Each step must be justified by a rule of the logic, by a definition, or by a theorem already proved, and each of those in turn rests on earlier ones, down to a short list of basic rules and axioms. Nothing is taken as obvious.

This makes formal proofs much longer than written ones, and much more tedious to produce by hand. A proof assistant exists to make that work manageable and to check the result.

Interactive

The word assistant describes how the work is done. A person states a theorem and starts to prove it. At each point the program shows what is still to be proved, called the goal, and the facts available for proving it. The person supplies a step. The program either accepts the step and shows the new goal, or refuses it and says why. The work ends when no goal is left. The page on holes and goals shows this exchange in Lean.

The person does not have to write every tiny step. Most proof assistants offer commands, called tactics, that carry out many small steps at once: split a statement into cases, rewrite with an equation, try a standard argument. Whatever a tactic produces is still checked before it is accepted.

Lean was started in 2013 by Leonardo de Moura at Microsoft Research as an interactive theorem prover, the technical name for a proof assistant. Lean 4 is a reimplementation of it written in Lean itself.

Finding a proof and checking one

A computer can help with a proof in two different ways. It can find a proof, or it can check one that someone has supplied.

Automated theorem provers are built for finding. Given a statement in a restricted form, they search for a proof by themselves, using fixed procedures for propositional and first-order logic and for particular kinds of problem such as arithmetic over the integers. They can be very fast, but their range is limited: one cannot set up a whole mathematical theory inside them. The authors of Theorem Proving in Lean 4 also note that such systems often favour speed over a guarantee that their answers are correct, and that a fault in them can be hard to detect.

A proof assistant is built for checking. It sets a high standard, every step justified, and in return it asks much more of the person using it. In most cases the person supplies the ideas, and the machine supplies the bookkeeping and the verdict.

The line is not sharp. Lean includes automation that searches for proofs of particular kinds of statement, and the project's stated aim is to place such tools inside a system whose final product is a fully checked proof. What a search procedure finds is not trusted because it was found; it is accepted only after it has been checked, so an honest fault in the search can cost a proof but does not let a wrong one through. The page on automation and its limits says more.

Other proof assistants

Lean is one of several mature proof assistants. They differ in the logic they check, in how a user writes proofs, and in the libraries built for them.

• Rocq, called Coq until 2025, began in 1984 at INRIA-Rocquencourt in the work of Thierry Coquand and Gérard Huet. It checks proofs in a Calculus of Inductive Constructions, a type theory of the same family as Lean's. The change of name was completed with version 9.0 on 12 March 2025. A proof of the four colour theorem was checked in it.
• Isabelle describes itself as a generic proof assistant. It was originally developed at the University of Cambridge and the Technische Universität München.
• HOL Light was written by John Harrison. It is implemented in the programming language OCaml and has a much simpler logical core than other systems of its family. Isabelle and HOL Light both descend from Robin Milner's LCF system of the 1970s. The formal proof of the Kepler conjecture was checked with the two together.
• Agda is a dependently typed programming language, an extension of Martin-Löf's type theory, which can be used as a proof assistant.

None of these is a standard that the others fall short of. The choice between them is a choice of logic, of style and of library.

What "checked" means

When Lean accepts a theorem, the claim it makes is narrow and exact. The statement has been read according to the definitions and notation in force, and Lean's kernel, the small part of the program that has the last word, has accepted a proof of that statement from the definitions, theorems and axioms in the file and in the files it imports.

That is a strong claim. It leaves out several things.

It does not say the statement means what its author intended. Lean's reference manual separates two questions: whether a theorem has a valid proof, and what the theorem's statement means. The checker answers only the first. If a definition misreads the idea it was meant to capture, the theorem is a true statement about the wrong thing. The team that formalised the Kepler conjecture listed this first among the questions an auditor must ask: did the right theorem get formalised? The page on stating the right thing takes this up.

It does not say the axioms are true. A proof is valid relative to the axioms it uses. Lean can list them for any theorem; see what the axioms are.

It assumes the checker is correct. The part that must be trusted is kept small on purpose, and independent checkers exist, but it is still a program. See what has to be trusted.

It assumes honesty in what is imported. A check of one file trusts the libraries it uses, unless those are checked again as well. Lean's manual describes stronger checks, step by step, for cases where a proof may have been written to mislead.

Within these limits, "checked" means that no step was skipped and no case was forgotten. That is more than a careful human reader can promise, and the next page explains why mathematics came to want it.

Next

• Checking instead of convincing: how mathematics has accepted proofs, and what a mechanical check adds.
• The small trusted core: the part of Lean that has the last word.