4.1.1. Historical context🔗

The correspondence is named after Haskell Curry and William Alvin Howard, but its roots go deeper:

• Haskell Curry (1934) observed that the types of combinators in combinatory logic correspond to axiom schemes in propositional logic.

• William Howard (1969, published 1980) extended this to a full correspondence between natural deduction and simply typed lambda calculus.

• Nicolaas Govert de Bruijn independently discovered the correspondence while developing the Automath system (1968), one of the first proof checkers.

• Per Martin-Löf (1971 onwards) developed intuitionistic type theory, extending the correspondence to predicate logic with dependent types.

Lean's type theory is a descendant of Martin-Löf's work, enriched with features from the Calculus of Inductive Constructions (as used in Coq).

4.1.2. Propositions as types, proofs as terms🔗

In Lean, every proposition P : Prop is a type. A proof of P is a term h : P -- that is, an inhabitant of the type P. If a type is inhabited, the corresponding proposition is true; if it is empty, the proposition is false.

This idea is sometimes called the BHK interpretation (Brouwer-Heyting-Kolmogorov), which gives a constructive meaning to the logical connectives. Let us see how each connective maps to a type-theoretic construction.

4.1.3. Implication = function type🔗

The most fundamental instance of the correspondence: implication corresponds to the function type.

If P and Q are propositions, then P → Q is the type of functions from P to Q. A proof of P → Q is a function that, given a proof of P, produces a proof of Q.

Here is the same theorem proved in two ways -- by tactic and by term:

A proof of P → Q → R is a function of two arguments (curried):

4.1.4. Conjunction = product type🔗

The conjunction P ∧ Q corresponds to the product type P × Q (more precisely, it is defined as a structure with two fields). A proof of P ∧ Q is a pair ⟨hP, hQ⟩ consisting of a proof of P and a proof of Q.

Note that And.intro is the constructor, and And.left / And.right (equivalently .1 / .2) are the projections -- exactly like a product type.

4.1.5. Disjunction = sum type🔗

The disjunction P ∨ Q corresponds to the sum type (coproduct). A proof of P ∨ Q is either a proof of P (tagged with Or.inl) or a proof of Q (tagged with Or.inr).

4.1.6. Negation = function to False🔗

Negation ¬P is defined as P → False. That is, a proof of ¬P is a function that takes a hypothetical proof of P and derives a contradiction.

4.1.7. Universal quantifier = dependent function type (Pi type)🔗

The universal quantifier ∀ (x : α), P x corresponds to the dependent function type (Pi type) (x : α) → P x. A proof is a function that, for each x : α, produces a proof of P x.

Notice that in Lean, ∀ and the dependent arrow → are actually the same thing. When the codomain does not depend on the input, the dependent function type degenerates to the ordinary function type.

4.1.8. Existential quantifier = dependent pair type (Sigma type)🔗

The existential quantifier ∃ (x : α), P x corresponds to the dependent pair type. A proof consists of a witness a : α together with a proof that P a holds.

Note: There is an important distinction between ∃ (which lives in Prop) and Σ (which lives in Type). We discuss this further in the chapter on dependent types.

4.1.9. Nonempty and propositional truncation🔗

The Curry-Howard view says "to prove ∃ x, P x, give an x and a proof of P x". But sometimes you want to express that some element of a type α exists, without committing to a specific witness. For this Lean has the typeclass

Nonempty α is a proposition: it asserts only that α has at least one element, but it does not give you one. This is the propositional truncation of α: it forgets the witness, keeping only the bare existence claim.

To extract data from a Nonempty (i.e., to actually obtain a term of α), you must use Classical.choice, an axiom of Lean's type theory:

This is a real axiom: constructively, knowing only that α is nonempty does not let you pick an element. Classical.choice turns the propositional fact into honest data, at the cost of being nonconstructive.

This pair (Nonempty.intro, Classical.choice) is the prototypical example of moving data between Type and Prop. In Mathlib it is the foundation for many "exists, therefore choose one" arguments, and the reason noncomputable appears so often.

A related construction is Squash α, the explicit propositional truncation of α -- it has a single constructor Squash.mk a for any a : α, and sits at the boundary between Prop and Type.

4.1.10. How tactic proofs build terms behind the scenes🔗

When you write a tactic proof in Lean, the tactic block constructs a term behind the scenes. Every tactic manipulates the proof state and ultimately produces a term of the goal type. You can use show_term (or look at the output of #print) to see what term a tactic proof generates.

Here is a more complex example where the term proof is less obvious:

4.1.11. Summary table🔗

Here is a summary of the Curry-Howard dictionary:

Understanding this correspondence is key to becoming fluent in Lean: when you write a tactic proof, you are really constructing a term; when you write a term proof, you are programming a function. The two perspectives are equivalent, and switching between them often leads to deeper understanding.

4.2.1. What makes dependent types special🔗

In a simply typed language (like Haskell without extensions, or basic OCaml), the type of a function's output cannot depend on the value of its input -- only on the type of its input. For example, you can write f : ℕ → ℕ, but you cannot write a type that says "a list whose length equals the input n."

In a dependently typed language, you can do this. The type of the output may mention the input value. For example:

• (n : ℕ) → Fin n → ℝ is the type of a function that takes a natural number n and then an element of {0, 1, ..., n-1}, returning a real number.

• (n : ℕ) → Vector ℝ n is the type of a function that, given n, returns a vector of n real numbers.

This expressiveness is what allows Lean to serve simultaneously as a programming language and a theorem prover.

4.2.2. Pi types: dependent function types🔗

The Pi type (also written Π-type) is the type of dependent functions. In Lean, we write it as:

(x : α) → β x

where β : α → Sort u is a type family indexed by α. For each value a : α, the function returns a term of type β a. When β does not actually depend on x, this reduces to the ordinary function type α → β.

In Lean, ∀ is notation for Pi types when the codomain is a Prop:

Here is a concrete example of a dependent function:

Another important example: a function that, given a type, returns the identity function on that type. This is a function whose return type depends on its input:

4.2.3. Sigma types: dependent pair types🔗

The Sigma type (also written Σ-type) is the type of dependent pairs. In Lean, we write:

Σ (x : α), β x

or equivalently (x : α) × β x. A term of this type is a pair ⟨a, b⟩ where a : α and b : β a. Note that the type of the second component depends on the value of the first component.

When β does not depend on x, the Sigma type reduces to the ordinary product type α × β.

4.2.4. Difference between Sigma and Exists🔗

This is a subtle but important distinction in Lean:

• Σ (x : α), β x lives in Type -- you can extract the witness and use it computationally.

• ∃ (x : α), P x lives in Prop -- the witness is "erased" and cannot be used in computations (only in proofs).

This reflects the principle of proof irrelevance: in Prop, the specific proof does not matter, only whether the proposition is true or false. In Type, the data matters.

Mathematically, Σ is like a disjoint union (indexed coproduct), while ∃ is the propositional truncation thereof. In practice:

• Use ∃ when you only need to know that a witness exists (typical in mathematics).

• Use Σ when you need to actually compute with the witness (typical in programming).

4.2.5. Vectors indexed by length🔗

A classic example of dependent types is the type of vectors (lists of a fixed length). In Mathlib, one way to represent a vector of length n with entries in α is as a function Fin n → α, where Fin n is the type with exactly n elements {0, 1, ..., n-1}.

The advantage of this representation is that indexing is always safe: you cannot access index 5 of a 3-element vector, because 5 is not a term of type Fin 3. The type system prevents out-of-bounds errors at compile time.

4.2.6. Matrices as dependent types🔗

Matrices are a natural extension. An m × n matrix with entries in α can be represented as a function Fin m → Fin n → α, or equivalently as Matrix (Fin m) (Fin n) α in Mathlib:

In Mathlib, matrix multiplication is only defined when the dimensions match. If A is an m × n matrix and B is an n × p matrix, then A * B is an m × p matrix. The dependent types enforce that the inner dimensions agree -- a dimension mismatch is a type error, caught at compile time.

4.2.7. Type families🔗

A type family is simply a function that returns a type. Type families are pervasive in Lean and Mathlib:

In mathematical formalization, type families appear everywhere. For instance, the fiber of a function f : α → β over a point b : β is the subtype {a : α // f a = b}, which is a type family indexed by β.

4.2.8. Subtypes🔗

The subtype {x : α // P x} is a special case of a Sigma type where P : α → Prop. It represents elements of α satisfying predicate P. Since the second component is a proof (in Prop), subtypes enjoy proof irrelevance: two elements of {x : α // P x} are equal if and only if their first components are equal.

This is how many mathematical objects are defined in Mathlib. For example, the type of prime numbers could be defined as {n : ℕ // Nat.Prime n}.

4.2.9. Why dependent types matter🔗

Dependent types make Lean strictly more expressive than simply-typed languages like Haskell or OCaml. Here are some things you can express with dependent types that you cannot express in simply-typed languages:

1. Length-indexed collections: The type system guarantees that head is never called on an empty list, that matrix dimensions match in multiplication, etc.

2. Precise specifications: You can write a sorting function whose type guarantees that the output is sorted and is a permutation of the input.

3. Mathematical theorems: The type ∀ (n : ℕ), ∃ (p : ℕ), p > n ∧ Nat.Prime p expresses Euclid's theorem (infinitely many primes). A term of this type is a proof.

4. Safe APIs: You can define a division function (a : ℤ) → (b : ℤ) → b ≠ 0 → ℤ that requires a proof of non-zero denominator. No runtime exceptions possible.

The price of this expressiveness is that type checking becomes undecidable in general (though Lean uses various heuristics to make it practical). But for mathematics, the payoff is enormous: the type system itself becomes a logic in which we can state and prove theorems.

4.3.1. The universe hierarchy🔗

In Lean, every type itself has a type. To avoid paradoxes (like Russell's paradox), types are organized into a hierarchy of universes:

• Prop is the universe of propositions. It is also called Sort 0.

• Type 0 (or simply Type) is the universe of "ordinary" types. It is also called Sort 1.

• Type 1 is the universe of types whose elements are themselves types in Type 0. It is Sort 2.

• In general, Type n is Sort (n + 1).

The key rule is that Sort n : Sort (n + 1), so:

This hierarchy prevents Type : Type, which would lead to Girard's paradox (a type-theoretic analogue of Russell's paradox).

4.3.2. Prop vs Type: proof irrelevance🔗

The universe Prop has a special property that distinguishes it from all Type n: proof irrelevance. This means that if P : Prop and h1 h2 : P, then h1 = h2. In other words, all proofs of the same proposition are considered equal.

This is a deliberate design choice. It means:

• You cannot pattern-match on a proof to extract computational data.

• Proofs can be erased at compile time without affecting program behavior.

• Two mathematical proofs of the same theorem are interchangeable.

The distinction between Prop and Type corresponds to the mathematical distinction between "asserting that something exists" (Prop) and "constructing a specific example" (Type).

4.3.3. Universe polymorphism🔗

Many definitions in Lean need to work across multiple universe levels. For this, Lean supports universe polymorphism. You can declare universe variables and use them in definitions:

In Mathlib, many definitions are universe-polymorphic. For example, Set α works regardless of which universe α lives in. When you see {α : Type*}, the * means "at any universe level" -- this is Lean's way of automatically introducing a universe variable.

4.3.4. The axioms of Lean🔗

Lean's kernel is built on the Calculus of Inductive Constructions, which by itself is quite weak. To support the mathematics we want to formalize, Lean adds a small number of axioms. Let us examine each one.

4.3.5. Constructive vs classical logic🔗

By default, Lean's type theory is constructive: proofs must provide explicit witnesses and constructions. The axiom of choice introduces classical reasoning, which allows non-constructive arguments.

4.3.6. Comparison with ZFC set theory🔗

Most mathematicians are (at least implicitly) trained in ZFC set theory. Here are the key differences from Lean's type theory:

A key practical difference: in ZFC, you can ask nonsensical questions like "is 3 ∈ π?" and get an answer. In Lean, comparing objects of different types is a type error, which catches many mistakes early.

Both foundations are equiconsistent for most of mathematics. Nearly everything that can be formalized in ZFC can also be formalized in Lean's type theory (and vice versa).

4.3.7. Brief mention of other type theories🔗

Lean's type theory is one of several:

• Simply typed lambda calculus (Church, 1940): No dependent types. Foundation for Haskell, OCaml.

• System F (Girard, Reynolds, 1970s): Adds polymorphism but not full dependent types.

• Martin-Löf Type Theory (MLTT, 1971+): The origin of dependent types in proof assistants. Used in Agda.

• Calculus of Inductive Constructions (CoIC): Used in Coq/Rocq. Lean's type theory is closely related.

• Homotopy Type Theory (HoTT, 2013): Interprets types as topological spaces and equality as paths. Adds the univalence axiom (due to Voevodsky): equivalent types are equal. This is incompatible with Lean's proof irrelevance for Prop, so HoTT uses different proof assistants (Agda, cubical Agda, or specialized Lean forks).

• Cubical Type Theory (2015+): Makes HoTT computational by using a cube category to model paths.

For this course, Lean's type theory (CIC + proof irrelevance + quotients + choice) is the framework we work in. It is expressive enough to formalize virtually all of modern mathematics, as the Mathlib library demonstrates.

4.4.1. Defining structures🔗

A structure is a special case of an inductive type with exactly one constructor and named fields. Here is a simple example:

This defines a type Point with two fields, x and y, both of type Float. We create values of type Point using anonymous constructor syntax or by naming the constructor explicitly:

All three syntaxes create a Point. The angle brackets ⟨...⟩ (typed \< and \>) are the anonymous constructor.

4.4.2. Accessing fields and dot notation🔗

We access fields using dot notation:

We can also define functions in the Point namespace, and then call them with dot notation:

This works because Lean sees that p2 has type Point, so it looks for Point.distToOrigin.

4.4.3. Updating structures🔗

We can create a new structure value based on an existing one, changing only some fields. This uses the with keyword:

Since structures are immutable (as everything in functional programming), this creates a new Point rather than modifying p1.

4.4.4. Structures with default values🔗

Fields can have default values:

4.4.5. Extending structures🔗

One structure can extend another, inheriting all of its fields:

This is particularly important in Mathlib, where the algebraic hierarchy uses structure extension extensively. For example, CommRing extends Ring, which extends Semiring, and so on.

4.4.6. Mathematical examples🔗

Structures are natural for representing mathematical objects. Here is a complex number type:

Here is a structure representing a linear map between two types that have addition and scalar multiplication:

Notice that the structure contains both data (the function toFun) and a property (map_add). This pattern of bundling data with properties is fundamental to how Mathlib organizes mathematics.

4.4.7. Inductive types vs structures🔗

When should you use inductive and when structure?

• Use structure when your type has a single constructor with named fields. Examples: points, complex numbers, algebraic structures.

• Use inductive when your type has multiple constructors. Examples: natural numbers, lists, trees, Option, Bool.

A structure is syntactic sugar for an inductive type with one constructor. The definition

structure Point where
  x : Float
  y : Float

is essentially equivalent to

inductive Point where
  | mk : Float → Float → Point

but the structure version gives us named fields, dot notation, default values, and the extends mechanism.

4.4.8. Using deriving🔗

When we define a new type, Lean can automatically generate certain instances for us using deriving:

Without deriving Repr, the #eval command would not know how to print a Student. The deriving clause tells Lean to automatically create a Repr instance. Other commonly derived instances include BEq (Boolean equality), Hashable, and Inhabited.

4.4.9. Namespaces🔗

Every structure automatically creates a namespace. When we defined Point, Lean created the namespace Point containing Point.mk, Point.x, and Point.y. We can add more definitions to this namespace:

Using namespaces keeps related functions organized and enables dot notation.

4.5.1. The problem typeclasses solve🔗

Consider the + operator. It works on natural numbers, integers, real numbers, matrices, polynomials, and many other types. How does Lean know which + to use?

One approach would be to define different functions: addNat, addInt, addReal, etc. But that would be extremely tedious. Instead, Lean uses typeclasses: there is a single Add typeclass, and each type that supports addition provides an instance of Add.

When you write a + b, Lean looks at the types of a and b, finds the appropriate Add instance, and uses it. This process is called instance resolution and happens automatically.

4.5.2. Defining typeclasses🔗

A typeclass is defined using the class keyword. Here is a simplified version of how Add might be defined:

This says: for any type α, an instance of MyAdd α provides a function myAdd : α → α → α. The class keyword is almost the same as structure -- in fact, every class is internally a structure. The difference is operational:

• A structure is constructed and passed explicitly: you write ⟨...⟩ or call its named projections.

• A class is also a structure, but Lean's instance resolution will synthesize one for you whenever a function expects an [Add α] argument. You never write the instance argument by hand.

So the rule of thumb is: use structure when the value is part of the data the user manipulates (a Point, a Person, a RingHom); use class when the value is a canonical piece of structure attached to a type (a Group instance on ℤ, an Add instance on ℕ) and you want Lean to find it automatically.

4.5.3. Creating instances🔗

We create instances using the instance keyword:

Now we can use MyAdd.myAdd on natural numbers and integers, and Lean will automatically find the right instance.

Let us define a custom type and give it an Add instance:

We defined two instances: Add Vec2 so we can use +, and ToString Vec2 so Lean can print Vec2 values.

4.5.4. The square bracket notation🔗

When a function needs a typeclass instance, we use square brackets [...] in its signature:

The [Add α] argument tells Lean: "find an Add instance for α automatically." We do not need to pass it explicitly; Lean's instance resolution handles it.

You can name the instance if you need to refer to it:

But usually the unnamed form [Add α] is preferred, since Lean resolves it behind the scenes.

4.5.5. Inspecting typeclass arguments with @🔗

When working with Mathlib, it is often useful to see all the implicit and typeclass arguments of a lemma. The @ symbol makes all arguments explicit:

#check mul_comm
-- mul_comm : ∀ {M : Type u_1} [inst : CommMonoid M] (a b : M), a * b = b * a

#check @mul_comm
-- @mul_comm : ∀ {M : Type u_1} → CommMonoid M → M → M → M = M

The first form shows [inst : CommMonoid M] in brackets, meaning it is found automatically. The @ version shows all arguments explicitly, which helps understand exactly what typeclass constraints are required.

4.5.6. The algebraic hierarchy in Mathlib🔗

Mathlib uses typeclasses to build an extensive hierarchy of algebraic structures. Here are some key ones, ordered roughly from weakest to strongest:

• Add α -- a type with an addition operation

• Mul α -- a type with a multiplication operation

• AddMonoid α -- a type with addition, an additive identity 0, and associativity

• Monoid α -- a type with multiplication, a multiplicative identity 1, and associativity

• Group α -- a monoid with inverses

• AddCommGroup α -- a commutative group under addition

• Ring α -- an additive commutative group with a multiplication that distributes over addition

• CommRing α -- a ring with commutative multiplication

• Field α -- a commutative ring where every nonzero element has an inverse

• LinearOrder α -- a type with a total order

Each of these is defined as a class that extends simpler classes. For example (simplified):

class Group (α : Type) extends Monoid α where
  inv : α → α
  inv_mul_cancel : ∀ a : α, inv a * a = 1

When you write a lemma that requires a CommRing, Lean automatically knows that it also has Add, Mul, AddCommGroup, etc., because of the extends chain.

The power of this system is that we can state and prove theorems at the most general level. For instance, mul_comm works for any CommMonoid, which includes ℕ, ℤ, ℚ, ℝ, ℂ, polynomial rings, matrix rings (when the base is commutative), and many more.

4.5.7. Defining multiple instances🔗

Let us build a more complete example. We define a type Mod3 representing integers modulo 3, and equip it with algebraic structure:

4.5.8. How instance resolution works🔗

When Lean encounters an expression like a + b where a b : α, it needs to find an instance of Add α. The resolution proceeds as follows:

1. Lean looks through all registered instances (those declared with instance).

2. It tries to unify the goal Add α with the type of each instance.

3. If an instance itself requires other instances (e.g., Add (Prod α β) might require Add α and Add β), Lean recursively resolves those.

4. If exactly one chain of instances leads to a solution, Lean uses it. If none or multiple exist, it reports an error.

This process is deterministic and happens at elaboration time (when Lean checks your code), not at runtime. So there is no performance penalty.

4.5.9. Practical tips🔗

• When you get an error like "failed to synthesize instance," it means Lean cannot find a required typeclass instance. Check that your type has the necessary instance defined.

• Use #check @lemma_name to see all implicit arguments and understand what instances a lemma requires.

• In Mathlib, most standard types (ℕ, ℤ, ℚ, ℝ, ℂ) have instances for all the common typeclasses. You rarely need to define instances for these.

• When defining your own types, provide instances for the typeclasses you need. Start with Repr (for printing), then Add, Mul, etc., as needed.

• The deriving mechanism can automatically generate instances for some typeclasses (like Repr, BEq, Hashable, Inhabited).