Glossary

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

Terms the pages of this edition define, each where it is first set out in bold, with the page that defines it and, where there is one, the page that explains it in plain language. The definitions here are short; the pages carry the working ones, with their sources. Symbols are on the notation page.

A

Automated theorem prover. A program built to find proofs by itself, for statements in a restricted form, rather than to check proofs that a person supplies. See What a proof assistant does.

Automath. The formal language for mathematics, and the project around it, that N. G. de Bruijn designed at Eindhoven in the late 1960s; its checkers confirmed proofs written out in full. See Automath; in plain language, Checking instead of convincing.

Axiom. A constant of a given type that is simply postulated; when its type is a proposition, an assumed proof of it. Lean cannot check that an axiom is consistent, and #print axioms lists the axioms a theorem rests on. See The three axioms; in plain language, What the axioms are.

Axiom K. Streicher's principle that every proof of a = a is Eq.refl a. It is equivalent to uniqueness of identity proofs, and in Lean it holds by definition. See Propositional equality.

B

Beta reduction. The rule that applying a function abstraction to an argument substitutes the argument for the bound variable. It is one of the reductions that make up definitional equality. See Definitional equality and Dependent function types.

Blueprint. A tool written by Patrick Massot that links a human-readable account of a proof, lemma by lemma, to its Lean counterparts, and draws their dependency graph with the progress of each. See The polynomial Freiman-Ruzsa conjecture.

C

Calculus of Inductive Constructions. The Calculus of Constructions extended with primitive inductive definitions. Coq, now Rocq, was named after it. See The Calculus of Constructions.

Comparator. A tool that checks a proposed proof against a theorem statement written beforehand in a trusted setting: it compiles the proof in a sandbox, exports it, replays the export with the Lean kernel or an independent checker, and confirms that exactly the stated theorems were proved. See Proof export and independent checkers.

Condensed mathematics. The framework begun by Clausen and Scholze that proposes condensed sets in place of topological spaces in the foundations of mathematics. The theorem checked in the Liquid Tensor Experiment belongs to it. See The Liquid Tensor Experiment.

Congruence closure. Grouping terms known to be equal, together with what follows from the rule that equal arguments give equal results. It is one of the methods of grind. See Decision procedures.

Constructive logic. A logic in which a proof of "P or Q" must say which side holds, so that the law of the excluded middle is not available in general. Lean's logic without axioms is constructive. See Classical logic from choice; in plain language, What the axioms are and Propositions as types.

Constructor. One of the rules that make the values of an inductive type. The values of the type are exactly those its constructors make. See Inductive types and recursors; in plain language, Building things from constructors.

Context. A list of variables with their types, each type able to mention the variables before it. A typing judgment is made in a context. See Terms, types and judgments.

Conversion rule. The typing rule that a term of type $A$ also has every type definitionally equal to $A$. It is where computation enters typing. See Terms, types and judgments.

Course-of-values recursion. Structural recursion in which a call may use the results for any smaller argument, not only for the immediately smaller one. Lean provides it through the constructions below and brecOn. See Structural and well-founded recursion.

Curry–Howard correspondence. Another name for propositions as types, after two of the logicians who found it. See Propositions as types.

D

de Bruijn criterion. The requirement that a proof assistant's proofs can be checked independently by a small program, one that a person can inspect; named after N. G. de Bruijn. In Lean the small program is the Lean kernel. See The small trusted core and Checking instead of convincing and Automath.

de Bruijn factor. The ratio between the size of a formal text and the size of the informal original it renders, both compressed. For the Automath translation of Landau's Grundlagen it is about 3.7. See Automath.

de Bruijn index. A number standing for a bound variable: the count of binders between the variable and the binder that introduces it. In Lean the nearest binder has index 0. See Terms, types and judgments and Metaprogramming in Lean.

decide. The tactic that proves a statement by finding a procedure that decides it and running it. It works when the statement has no unknowns and such a procedure is available. See Decision procedures; in plain language, Automation and its limits.

Decision procedure. An algorithm that settles every question in a fixed class with yes or no. In Lean it is useful only when its yes comes with evidence the Lean kernel accepts. See Decision procedures.

Default instance. An instance tried when a search for instances would otherwise fail without selecting one. It is why fun x => x + 1 elaborates to a function on Nat. See Type classes and instance resolution and Elaboration.

Definitional equality. The equality that holds between two terms by computation and the unfolding of definitions, without proof. Lean's checker tests it for itself, and no proof records it. See Definitional equality; in plain language, Two kinds of equality.

Delta reduction. The rule that a defined constant equals its definition. See Definitional equality.

Dependent function type. The type of functions whose result type may depend on the argument, written (x : A) → B; also called a dependent product or Π-type. It is the only kind of function type in Lean's core theory: ordinary function types, "for all" and implication are special cases. See Dependent function types; in plain language, Types as specifications.

Dependent type. A type that depends on a value, such as the type of lists of a given length. See Types as specifications and Propositions as types.

do-notation. Lean's syntax for writing programs that use a monad in an imperative style, with sequencing, mutable local variables, loops and early return. A do block is translated into an ordinary term. See Monads and do-notation.

E

E-matching. Instantiating a theorem by matching its pattern against terms, up to the equalities known so far. It is one of the methods of grind. See Decision procedures.

Elaboration. The step that turns what a person types into a fully explicit term of Lean's core type theory, supplying omitted arguments, instances, coercions and universe levels. The program that does it, the elaborator, need not be trusted, because its output goes to the Lean kernel. See Elaboration; in plain language, The small trusted core and When Lean says no.

elan. The toolchain manager, which installs versions of Lean and selects the one a project names. A toolchain is the set of programs and files for one version of Lean. See Lake and Lean projects.

Equational law. An identity that a binary operation may satisfy for all values of its variables, such as the commutative law. A magma is a set with one such operation and no further rules; one law implies another when every magma satisfying the first satisfies the second. See The equational theories project.

Eta. For functions, the rule that $\lambda x.fx$ equals $f$; for structures, the rule that a value equals the constructor applied to its fields. Both are part of Lean's definitional equality. See Definitional equality and Dependent function types.

External checker. A second program, written separately, that reads a proof exported from Lean and checks it again. See Proof export and independent checkers; in plain language, What has to be trusted and Checking a proof again later.

F

Function extensionality. The principle that functions giving equal results on every argument are equal. In Lean it is a theorem, proved from quotients. See Propositional equality; in plain language, What the axioms are.

G

Global choice. The axiom Classical.choice: from a proof that a type has a value, it gives a value of the type. See The three axioms; in plain language, What the axioms are.

Goal. A statement still to be proved, with the hypotheses that may be used to prove it. In Lean's tactic framework each goal is a metavariable; the first in the list is the main goal. See The tactic framework; in plain language, Holes and goals and What a proof assistant does.

grind. A tactic that collects facts in one shared store and works on them with several methods at once, among them congruence closure, E-matching, case splits and solvers for arithmetic. See Decision procedures; in plain language, Automation and its limits.

H

Heterogeneous equality. An equality between terms whose types are not known to be definitionally equal, written a ≍ b in Lean 4.34.1. See Propositional equality.

Higher-order unification. Unification in which a metavariable stands for a function applied to arguments. It is undecidable in general, and decidable for patterns, in which a metavariable is applied only to distinct bound variables. See Metavariables and unification.

Hygiene. The property of Lean's macros that a name a macro introduces cannot capture a name the user wrote, nor the reverse. It is implemented by macro scopes, which tag each name a macro introduces. See Syntax extension and hygienic macros.

I

Implicit argument. An argument the caller does not write. An implicit argument is filled by unification; a strict implicit one likewise, but only once a later explicit argument is given; an instance-implicit one by instance resolution. See Dependent function types.

Impredicativity. The property of Prop that a proposition may quantify over all propositions, or over types at any level, and still be a proposition. Its opposite, predicativity, holds for the universes Type u. See Universes and Prop; in plain language, Why there is no type of all types.

Index. An argument of an inductive family that may differ from one constructor to another; a parameter is fixed across the whole definition. In a = b, b is an index. See Inductive types and recursors and Propositional equality.

Induction hypothesis. In a proof by induction on the natural numbers, the assumption that the statement holds for $k$, used in the induction step to prove it for $k+1$; the base case is the proof for 0. See Induction, as the machine sees it.

Inductive family. An inductive definition with indices, which defines a whole family of types at once. The notion is Dybjer's. See Inductive types and recursors.

Inductive type. A type whose values are exactly those made by its constructors. Apart from functions, universes and quotient types, which are built into Lean, every type in Lean is an inductive type or is defined from these. See Inductive types and recursors; in plain language, Building things from constructors.

Instance. A definition registered for a type class, which the elaborator finds by itself when a term needs it; for example, the definition that says how to add two values of given types. See Type classes and instance resolution; in plain language, When Lean says no.

Instance resolution. The search by which the elaborator finds instances, also called instance synthesis. Lean's is tabled. See Type classes and instance resolution.

Iota reduction. The rule that a recursor applied to a constructor reduces to the corresponding minor premise. It is part of definitional equality. See Inductive types and recursors and Definitional equality.

IR. The compiler's lower-level form of a definition, translated from LCNF, which Lean prints on request and which its interpreter runs. See The compiler and runtime.

L

Lake. The tool that ships with every version of Lean for compiling Lean code and fetching what a project depends on; a project organised for it is a Lake package. It records the exact version of each dependency in the file lake-manifest.json. See Lake and Lean projects; in plain language, A library of mathematics.

Large elimination. Eliminating a proof of a proposition into any universe, so as to produce data. Lean allows it only when the proposition is a syntactic subsingleton. See Proof irrelevance and subsingleton elimination.

Law of the excluded middle. The principle that every proposition is either true or false. It cannot be proved in Lean's logic without axioms; with choice and the two extensionality principles it can (Diaconescu's theorem). See Classical logic from choice; in plain language, What the axioms are.

LCNF. Lean Compiler Normal Form: the compiler's representation of a definition in A-normal form, in which every intermediate result is bound to a name. See The compiler and runtime.

Lean kernel. The type checker that decides whether a definition, theorem, axiom or inductive type may enter Lean's environment, its table of definitions and theorems. It is the small part of Lean that has to be trusted. It has no termination checker and performs no unification. See The Lean kernel; in plain language, The small trusted core.

Lean Kernel Arena. A site that runs checkers for Lean on the same exported tests, some to be accepted and some to be rejected, and publishes the results. See Proof export and independent checkers; in plain language, Checking a proof again later.

lean4export. A program that writes the constants of a Lean module, and everything they depend on, to a file of terms alone, for other checkers to read. See Proof export and independent checkers.

Lean4Lean. A type checker for Lean 4 written in Lean by Mario Carneiro, parts of which have been proved correct against a formalisation of Lean's type theory. See Proof export and independent checkers; in plain language, Checking a proof again later.

leanchecker. The program, part of the Lean toolchain, that replays every definition and theorem in compiled Lean files through the Lean kernel. See Proof export and independent checkers.

Locally nameless. The representation of terms with de Bruijn indices for bound variables and names for free ones, which Lean uses. See Terms, types and judgments.

M

Macro. A rule that rewrites one piece of syntax into another before it is given meaning. Macro expansion is interleaved with elaboration, and Lean's macros are hygienic. See Syntax extension and hygienic macros and Elaboration.

Mathlib. The single library of mathematics formalised in Lean and maintained by its community, begun in 2017 for Lean 3 and later translated to Lean 4. See A library of mathematics and Research mathematics.

Measure. A quantity that must be smaller at every recursive call, named with termination_by; it justifies a definition by well-founded recursion. See Structural and well-founded recursion; in plain language, Functions that always finish.

Metaprogram. A Lean program whose data is Lean itself: syntax, terms, goals and Lean's environment. Tactics and elaborators are metaprograms. See Metaprogramming in Lean.

Metatheory. What can be proved about Lean's type theory rather than in it; chiefly its consistency, which has been proved, for the type theory of Lean 3, relative to set theory with inaccessible cardinals. See Consistency and the metatheory.

Metavariable. A named hole in a term: a placeholder for a subterm not yet known, which may be filled only with a term whose free variables are in its local context. Metavariables are natural, synthetic or synthetic opaque, according to who may fill them. See Metavariables and unification; in plain language, Holes and goals.

Monad. A type constructor, with operations for sequencing computations, that Lean uses to represent effects such as failure, state, input and output as values. See Monads and do-notation.

Motive. The argument of a recursor that says what is produced, or proved, for each value. A recursor also takes one minor premise for each constructor, and the major premise, the value the recursion runs on. See Inductive types and recursors.

N

nanoda. A checker for exported Lean proofs written in Rust, developed independently of Lean. See Proof export and independent checkers; in plain language, Checking a proof again later.

Nested inductive type. An inductive type that occurs, in its own definition, as an argument of another inductive type, as in a tree whose nodes hold lists of subtrees. Lean's kernel accepts one by translating it into a mutual definition. See Inductive types and recursors.

O

omega. The tactic for linear arithmetic over the integers and the natural numbers, after Pugh's omega test. See Decision procedures; in plain language, Automation and its limits.

Opaque constant. A constant with a type and no definition that the Lean kernel may unfold. A partial definition enters the logic as one. See Structural and well-founded recursion.

P

partial. A mark for a recursive definition whose termination is not proved: it is compiled as written, and enters the logic as an opaque constant. See Structural and well-founded recursion.

Pattern matching. Defining a function by one case for each constructor of its argument's type. Lean checks that every case is covered. See Building things from constructors.

Pre-definition. The form a recursive definition takes first, elaborated as if the core language had recursion. The compiler uses it, and termination analysis turns it into a non-recursive term for the Lean kernel. See Structural and well-founded recursion.

Proof assistant. A program that checks proofs written in a formal language, step by step, while a person writes them. A formal language is a notation with fixed rules for what counts as a statement and what counts as a valid step. See What a proof assistant does.

Proof irrelevance. The rule that any two proofs of the same proposition are interchangeable. In Lean they are definitionally equal. The name goes back to the Automath project, in 1974. See Proof irrelevance and subsingleton elimination; in plain language, Propositions as types.

Proof object. A complete record of a proof, in which every step is explicit, that a small program can check. See Checking instead of convincing.

Proof state. The list of goals at a point in a tactic proof. The proof is complete when the list is empty. See Holes and goals and Tactics.

Proposition. A statement. In Lean a proposition is a type in the universe Prop, and its values are its proofs. See Propositions as types and Universes and Prop.

Propositional equality. The proposition a = b: an inductive family with a single constructor, whose proofs are terms. It differs from definitional equality, which the checker tests and no term records. See Propositional equality; in plain language, Two kinds of equality.

Propositional extensionality. The axiom propext: propositions that imply each other are equal. See The three axioms; in plain language, What the axioms are.

Propositions as types. The correspondence under which a statement is a type and a proof of it is a value of that type. See Propositions as types.

Q

Quotient type. A type whose elements are those of an existing type, with every pair related by a given relation made equal. Quotients are primitive in Lean, with one axiom, quotient soundness (Quot.sound). See Quotient types; in plain language, What the axioms are.

R

Ramified theory of types. The more elaborate of Russell's theories of types, set out in a paper of 1908. See Why there is no type of all types.

Recursor. The constant Lean derives from an inductive definition, which is at once the type's induction principle and its means of primitive recursion; also called its recursion principle. See Inductive types and recursors; in plain language, Building things from constructors and Induction, as the machine sees it.

Reducibility hint. The mark stored with every definition, opaque, abbrev, or regular with a definitional height, that decides which side Lean's kernel unfolds first when it compares two terms. See Definitional equality.

Reference counting. Lean's way of managing memory: each object counts the references to it and is freed when the count reaches zero. A value that is not shared may be changed in place, so code written as pure functions can run with updates in place. See The compiler and runtime.

Reflexivity. The principle that everything is equal to itself. The proof rfl proves an equation exactly when the two sides are definitionally equal. See Two kinds of equality.

Restricted elimination. The rule that a proof can be taken apart to produce data only when its proposition is a subsingleton. See Proof irrelevance and subsingleton elimination and Universes and Prop.

S

Setoid. A type with a chosen relation and a proof that the relation is reflexive, symmetric and transitive; Lean's Quotient is the quotient by a setoid's relation. See Quotient types.

simp. The simplifier: a tactic that rewrites the goal with the simp set, the theorems marked @[simp], each read as an equation from left to right. See Decision procedures; in plain language, Automation and its limits.

Specification. A precise statement of what is required of a program or a value. A type can serve as one. See Types as specifications and Software verification.

Strict positivity. The condition that the type being defined occur in the argument types of its constructors only to the right of every arrow, or as an argument of another inductive type. Lean's kernel enforces it, because a type breaking it would prove False. See Inductive types and recursors.

Structural recursion. Recursion in which every call is on a strict part of one fixed argument. Lean compiles it through the recursor, so no separate test of termination is needed. See Structural and well-founded recursion; in plain language, Functions that always finish.

Structure. An inductive type with exactly one constructor, whose arguments are called its fields. See Building things from constructors.

Subject reduction. The property that a term which type-checks still type-checks after it is reduced. Lean's typing, with the algorithmic definitional equality that the Lean kernel checks, lacks it. See Definitional equality.

Subsingleton. A proposition that, by its shape, can have at most one proof. Subsingleton elimination is the permission such a proposition has to be eliminated into any universe. See Proof irrelevance and subsingleton elimination and Inductive types and recursors.

Subtype. The type of the values of a given type that have a given property, written {x : A // p x}. Each of its values is a value together with a proof. See Types as specifications.

Syntax quotation. Syntax written inside `(...), used in a macro to match syntax or to produce it; antiquotations inside it are the holes. Each grammar rule belongs to a syntax category, such as term. See Syntax extension and hygienic macros.

Synthetic metavariable. A metavariable that unification avoids assigning, because another procedure, usually instance resolution, is responsible for it; the elaborator uses them for postponed work. A synthetic opaque metavariable is never assigned by unification; goals are of this kind. See Metavariables and unification and Elaboration.

T

Tabled typeclass resolution. Lean's method of instance resolution, which keeps a table from each subgoal to the solutions already found for it and reuses them. Its authors proposed it to remove the exponential cost of diamonds in a hierarchy of classes and the loops caused by cycles of instances. See Type classes and instance resolution.

Tactic. A program that constructs part of a proof term, acting on goals. The name is Milner's, from LCF: there a tactic was a function reducing a goal to subgoals, and tacticals combined tactics. See The tactic framework and LCF and the tactic idea; in plain language, Tactics.

Term. Anything in Lean's type theory: a number, a function, a type, a proposition, a proof. In a proof written as a term, the term is an expression whose type is the statement. See Terms, types and judgments; in plain language, Tactics.

Total function. A function defined on every argument, which returns in finitely many steps. Lean's logic treats every function as total. See Structural and well-founded recursion.

Transport. Obtaining, from a proof of a = b and a term whose type mentions a, the same term at b. It is derived from the eliminator of equality. See Propositional equality.

Type class. A structure whose values, the instances, Lean finds by itself: a description of what a type must provide. See Type classes and instance resolution; in plain language, A library of mathematics.

Type inference. Computing a type for a term in a context. Type checking, by contrast, decides whether a term has a given type. Lean's kernel is built around inference. See Terms, types and judgments.

Typing judgment. The basic statement of the theory, $\Gamma ⊢e:A$: in the context $\Gamma$, the term $e$ has type $A$. A term is well-typed when such a judgment can be derived for it. See Terms, types and judgments.

U

Unification. The search for values of metavariables that make two terms definitionally equal. See Metavariables and unification; in plain language, Holes and goals.

Uniqueness of identity proofs. The principle that any two proofs of a = b are equal. In Lean it holds by definitional proof irrelevance. See Propositional equality.

Universe. A type whose members are types; also called a sort. Lean's universes Sort u form a hierarchy without top, each a member of the next, with Prop at the bottom; they are not cumulative. See Universes and Prop; in plain language, Why there is no type of all types.

unsafe. A mark that frees a definition from Lean's restrictions, at the price that only other unsafe definitions may use it and no theorem may. See Structural and well-founded recursion.

W

Weak head normal form. The result of reducing a term at its head until no rule applies: a sort, a function type, an abstraction, a literal, a constructor application, or an application whose head cannot be unfolded or reduced. See Definitional equality.

Well-founded recursion. Recursion justified by a quantity, or a well-founded relation, that decreases at every call. A relation is well-founded when it has no infinite descending chain. See Structural and well-founded recursion; in plain language, Functions that always finish.

Z

Zeta reduction. The rule that a local definition equals its body with the defined value substituted. See Definitional equality.

Next

• Notation