Lean

Definition

Lean

Lean is a proof assistant and a functional programming language based on dependent type theory. Definitions construct terms; theorem proofs construct terms whose types are propositions. Its kernel checks that these terms have the claimed types.

Terms and types

The basic relation is t : T: the term t has type T. A type determines what terms can be used where; it is not merely a label attached to a variable.

• x : M says that x is an element of the type M.
• M : Type u says that M is itself a type in a universe at level u.
• P : Prop says that P is a proposition.
• h : P says that h is a proof of that proposition.

Types can depend on terms: in τ : L.Sentence, the type of τ depends on the particular language L. The dot here names an existing library declaration; it is not a built-in operation for mathematical sentences.

Functions and parameters

A term f : A → B has a function type. Applying it to a : A, written f a, produces a term of type B. The expression fun x => t constructs a function with input x and body t.

A dependent function has type (x : A) → B x: its result type depends on its input. Lean also writes this as ∀ (x : A), B x.

Multiple inputs are handled by currying: A → B → C means A → (B → C), and f a b means (f a) b.

The binder controls how an argument is supplied, not whether the function has that argument:

Binder	Argument handling
[[Knowledge/Explicit Parameter (Lean)|(x : T)]]	The caller normally supplies it.
[[Knowledge/Implicit Parameter (Lean)|{x : T}]]	Lean tries to infer it from type constraints.
[[Knowledge/Instance-Implicit Parameter (Lean)|[x : T]]]	Lean searches for an available instance of T.

The declaration of the function determines which convention its callers encounter. Instance search is explained below.

Definitions and proofs

def name : T := t names a term t of type T. Parameters written before the colon become inputs to that definition.

theorem name : P := h names a proof h of proposition P. Merely defining a proposition with def name : Prop := P does not prove it.

The propositions-as-types correspondence explains why functions also express reasoning:

• A proof of P → Q takes a proof of P and produces a proof of Q.
• A proof of ∀ x : A, P x takes an arbitrary x : A and produces a proof of P x.
• Given h : P → Q and hp : P, function application h hp is a proof of Q.

Thus implication and universal quantification use function types; they do not require an unrelated proof language.

Inductive types and structures

An inductive declaration defines a type through its constructors: the permitted ways to build its terms. Lean generates principles for defining functions and proving statements by considering those constructors. Recursive constructors give rise to induction hypotheses.

A structure is a record type: its constructor groups named fields into one value, and projections retrieve the fields. Fields can contain values, functions or proofs. This packages related information; it does not make that information automatically discoverable.

In mathlib, L.Structure M packages interpretations of language symbols on an already supplied domain M. The name belongs to the library; the record mechanism belongs to Lean.

Classes and instance search

A typeclass is a type registered for instance synthesis. The class declaration defines a structure and registers it for this mechanism.

An instance is a term made available to that search. The instance command registers one; [i : C] introduces one as a parameter; letI : C := value supplies one locally.

When a function requires an argument [i : C], Lean searches for an available term of type C and passes it. The function then uses that term just like any other argument. Merely having an ordinary parameter (i : C) does not register it for instance search.

This is why [I : L.Structure M] lets M ⊨ τ find the interpretation I: the library’s satisfaction machinery requests an instance of that type. M is still the domain, not the whole mathematical structure.

Elaboration and the kernel

Elaboration turns the source you write into expressions with names resolved and omitted information supplied:

Notation, inferred arguments and instance search make source expressions shorter. They do not remove the underlying arguments or allow ill-typed expressions past the kernel.

Kernel acceptance is relative to the axioms used. sorry introduces an admitted proof through sorryAx; a file accepted with sorry does not establish the unfinished claim. #print axioms theoremName reports a theorem’s axiom dependencies.

Tactics construct proof terms

A by block uses tactics to construct a term of the required type. A goal consists of a target type and a local context containing available variables and hypotheses.

• exact supplies a term of the target type.
• apply uses a function or theorem whose conclusion matches the target and creates goals for missing premises.
• have introduces an intermediate result; obtain extracts information from a hypothesis.
• rw, unfold and simp transform expressions using equalities or definitions.
• funext reduces function equality to pointwise equality.
• induction uses the type’s induction principle; generalising induction controls what the induction hypothesis quantifies over.

Tactics are proof-building tools, not additional unchecked inference rules. Their completed proof terms are checked by the kernel.

Reading unfamiliar Lean

Start from the declaration rather than guessing from the notation:

1. Go to definition to find what a name or notation refers to.
2. Use #check name to inspect its type and parameters.
3. Use #print name to inspect its declaration, including its body when available.
4. Read (x : T), {x : T} and [x : T] to identify how its arguments are supplied.
5. If printed notation hides the mechanism, set_option pp.all true in #check name exposes more of the underlying expression.

Separate Lean’s language mechanisms—functions, inductive types, records and instances—from library declarations built using them, such as Language, L.Structure and satisfaction.