Category Theory & Type Theory

Advanced Topics » Category Theory & Type Theory

Category theory studies mathematical structure through the structure-preserving maps (morphisms) between objects rather than through the objects’ elements. Type theory studies formal systems of terms classified by types, and serves both as a foundation for programming languages and as an alternative foundation for mathematics. The two are linked by the Curry-Howard-Lambek correspondence: intuitionistic propositions, types, and objects of a cartesian closed category are three presentations of the same structure, as are proofs, programs, and morphisms. This page covers the core categorical vocabulary (categories through monads), the lambda calculus and its type systems, the correspondence itself, dependent type theory, and the proof assistants that implement it.

Overview

The three-way dictionary

The table below is the organizing idea of the page. Each row is one concept seen from logic, from programming, and from category theory; later sections develop each column.

Dependencies between topics

flowchart TD
    CAT["Categories"] --> FUN["Functors and natural transformations"]
    FUN --> YON["Yoneda lemma"]
    FUN --> UNIV["Universal properties: limits, colimits, exponentials"]
    UNIV --> ADJ["Adjunctions"]
    ADJ --> MON["Monads"]
    LAM["Untyped lambda calculus"] --> STLC["Simply typed lambda calculus"]
    STLC --> POLY["Polymorphism: Hindley-Milner, System F"]
    STLC --> CH["Curry-Howard"]
    UNIV --> CHL["Curry-Howard-Lambek: CCCs"]
    CH --> CHL
    CH --> DTT["Dependent type theory"]
    POLY --> DTT
    DTT --> HOTT["Homotopy type theory"]
    DTT --> PA["Proof assistants: Lean, Rocq, Agda"]

Categories

A category keeps only the arrows between objects and how they compose. Everything that can be said about an object is said through the morphisms into and out of it, which is why the same definitions apply unchanged to sets, groups, topological spaces, types, and propositions.

Definition. A category $\mathcal{C}$ consists of

• a collection of objects $\mathrm{ob}(\mathcal{C})$;
• for each pair of objects $A, B$ a collection $\mathrm{Hom}_{\mathcal{C}}(A, B)$ of morphisms $f : A \to B$;
• a composition operation and an identity morphism $\mathrm{id}_A$ for each object,

subject to associativity and the unit laws: for all $f : A \to B$, $g : B \to C$, $h : C \to D$,

A category is locally small if every $\mathrm{Hom}(A, B)$ is a set, and small if in addition $\mathrm{ob}(\mathcal{C})$ is a set. The distinction matters for statements such as the Yoneda lemma and for completeness results; Set itself is locally small but not small.

Examples

The monoid and preorder examples give two useful readings: a category is a many-object monoid, and a category is a preorder in which it matters which proof of $a \le b$ you have. The Hask example is only approximately a category: seq and non-termination break some equations (for example, $\eta$-equality for functions), so reasoning about Haskell categorically is usually done in an idealized total fragment.

Special morphisms

The Set intuitions do not transfer in general. In Ring the inclusion $\mathbb{Z} \hookrightarrow \mathbb{Q}$ is both mono and epi (a ring map out of $\mathbb{Q}$ is determined by its values on $\mathbb{Z}$) but is not an isomorphism.

Duality

Every category $\mathcal{C}$ has an opposite category $\mathcal{C}^{\mathrm{op}}$ with the same objects and all arrows reversed: $\mathrm{Hom}{\mathcal{C}^{\mathrm{op}}}(A, B) = \mathrm{Hom}{\mathcal{C}}(B, A)$. Because the axioms of a category are symmetric under reversal, every theorem has a dual obtained by reversing arrows: products become coproducts, monos become epis, limits become colimits, left adjoints become right adjoints. A proof of one statement is a proof of its dual.

Functors and Natural Transformations

Functors are the structure-preserving maps between categories; natural transformations are the maps between functors. Categories, functors, and natural transformations together form the 2-category Cat.

Definition. A functor $F : \mathcal{C} \to \mathcal{D}$ sends each object $A$ to an object $F(A)$ and each morphism $f : A \to B$ to a morphism $F(f) : F(A) \to F(B)$, preserving identities and composition:

A contravariant functor from $\mathcal{C}$ to $\mathcal{D}$ is a functor $\mathcal{C}^{\mathrm{op}} \to \mathcal{D}$. For a locally small $\mathcal{C}$ the hom-functors $\mathrm{Hom}(A, -) : \mathcal{C} \to \mathbf{Set}$ (covariant) and $\mathrm{Hom}(-, B) : \mathcal{C}^{\mathrm{op}} \to \mathbf{Set}$ (contravariant) are the prototypical examples. A functor is faithful or full when it is injective or surjective on each hom-set; an equivalence of categories is a full, faithful functor that is essentially surjective on objects. Equivalence, not isomorphism, is the correct notion of “sameness” for categories.

In a functional language, a type constructor with a lawful map is an endofunctor on the category of types. The functor laws are the familiar fmap laws:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

-- Laws (not checked by the compiler):
--   fmap id      == id
--   fmap (g . f) == fmap g . fmap f

instance Functor [] where
  fmap = map

Definition. Given functors $F, G : \mathcal{C} \to \mathcal{D}$, a natural transformation $\eta : F \Rightarrow G$ is a family of morphisms $\eta_A : F(A) \to G(A)$, one per object, such that for every $f : A \to B$ the naturality square commutes:

Naturality expresses that $\eta$ is defined uniformly, without choices that depend on the particular object. In programming, a polymorphic function eta :: forall a. f a -> g a between functors is automatically natural by parametricity (Reynolds 1983; Wadler’s “Theorems for free!”, 1989). For example reverse :: [a] -> [a] and listToMaybe :: [a] -> Maybe a satisfy fmap f . eta == eta . fmap f without any proof obligation.

The Yoneda lemma

Lemma (Yoneda). For a locally small category $\mathcal{C}$, a functor $F : \mathcal{C} \to \mathbf{Set}$, and an object $A$, there is a bijection, natural in $A$ and $F$,

Proof sketch. Given $x \in F(A)$, define $\alpha_B(f) = F(f)(x)$ for $f : A \to B$; this is natural by functoriality of $F$. Conversely, naturality forces $\alpha_B(f) = \alpha_B(f \circ \mathrm{id}_A) = F(f)(\alpha_A(\mathrm{id}_A))$, so $\alpha$ is determined by the single element $\alpha_A(\mathrm{id}_A)$.

Two consequences are used constantly:

• The Yoneda embedding $A \mapsto \mathrm{Hom}(-, A)$ is a full and faithful functor $\mathcal{C} \to \mathbf{Set}^{\mathcal{C}^{\mathrm{op}}}$, so every category embeds in a category of presheaves. This is the categorical analogue of Cayley’s theorem.
• Objects are determined by their arrows: $A \cong B$ if and only if $\mathrm{Hom}(-, A) \cong \mathrm{Hom}(-, B)$ naturally. This is why a universal property determines an object up to unique isomorphism.

In Haskell the lemma says that forall b. (a -> b) -> f b is isomorphic to f a for any functor f; the isomorphism is the basis of the “Yoneda” and codensity optimizations for fusing repeated fmaps:

{-# LANGUAGE RankNTypes #-}
newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)

toYoneda :: Functor f => f a -> Yoneda f a
toYoneda fa = Yoneda (\k -> fmap k fa)

fromYoneda :: Yoneda f a -> f a
fromYoneda (Yoneda y) = y id          -- alpha_A(id_A)

Universal Constructions

Products, disjoint unions, quotients, free objects, and function spaces are each the solution of a mapping problem that is unique up to unique isomorphism. Category theory states such universal properties once, for all categories.

Products and coproducts

Definition. A product of $A$ and $B$ is an object $A \times B$ with projections $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$ such that for every object $X$ and pair of maps $f : X \to A$, $g : X \to B$ there is a unique $\langle f, g \rangle : X \to A \times B$ with

The coproduct $A + B$ is the dual: injections $\iota_1 : A \to A + B$, $\iota_2 : B \to A + B$ and, for any $f : A \to X$, $g : B \to X$, a unique copairing $[f, g] : A + B \to X$. In Set these are the cartesian product and the disjoint union; in Vect$_k$ finite products and coproducts coincide as the direct sum (a biproduct); in a preorder they are meets and joins.

In a functional language the product is the pair type and the coproduct is the tagged-union type. The uniqueness clause corresponds to the $\eta$-laws: a function into a pair is determined by its two components, and a function out of a sum is determined by its two cases.

pair :: (x -> a) -> (x -> b) -> x -> (a, b)     -- <f, g>
pair f g x = (f x, g x)

either :: (a -> c) -> (b -> c) -> Either a b -> c   -- [f, g]
either f _ (Left a)  = f a
either _ g (Right b) = g b

Limits and colimits

Products and coproducts are special cases of limits and colimits of a diagram $D : J \to \mathcal{C}$. A limit is a universal cone over $D$ (an object with compatible maps into every object of the diagram); a colimit is a universal cocone (compatible maps out of it).

A category is complete (cocomplete) if it has all small limits (colimits). Set, Grp, and Top are both. A category has all finite limits if and only if it has a terminal object and pullbacks.

Exponentials and cartesian closed categories

Definition. In a category with binary products, an exponential of $B$ by $A$ is an object $B^A$ with an evaluation map $\mathrm{ev} : B^A \times A \to B$ such that every $f : C \times A \to B$ factors uniquely as $\mathrm{ev} \circ (\lambda f \times \mathrm{id}_A)$ for some $\lambda f : C \to B^A$. Equivalently, there is a natural bijection

which is currying. A cartesian closed category (CCC) has a terminal object, binary products, and all exponentials. Set, the category of small categories, and every presheaf category are cartesian closed; Top is not (compactly generated spaces are the usual fix). CCCs are exactly the categorical models of the simply typed lambda calculus with products, a theorem due to Lambek (Lambek and Scott, 1986).

Initial algebras and recursion

For an endofunctor $F$, an $F$-algebra is an object $X$ with a map $F(X) \to X$. An initial algebra $\mu F$, when it exists, is the initial object among $F$-algebras. Lambek’s lemma says its structure map $F(\mu F) \to \mu F$ is an isomorphism, so $\mu F$ is a least fixed point of $F$.

Inductive data types are initial algebras. Lists over $A$ are the initial algebra of $F(X) = 1 + A \times X$: the structure map combines [] and (:), and for any other algebra $[z, s] : 1 + A \times X \to X$ the unique algebra homomorphism out of lists is foldr s z. This unique map is called a catamorphism, and uniqueness is what justifies fold-fusion laws used in program calculation. Dually, final coalgebras $\nu F$ model infinite and coinductive data (streams) and support anamorphisms (unfolds).

Adjunctions

An adjunction is a pair of functors in opposite directions that are inverse “up to a universal mapping property” rather than up to isomorphism. Free constructions, currying, quantifiers, and Galois connections are all adjunctions.

Definition. Functors $F : \mathcal{C} \to \mathcal{D}$ and $G : \mathcal{D} \to \mathcal{C}$ form an adjunction $F \dashv G$ ($F$ left adjoint, $G$ right adjoint) if there is a bijection, natural in $A \in \mathcal{C}$ and $B \in \mathcal{D}$,

Equivalently, there are natural transformations, the unit $\eta : \mathrm{Id}{\mathcal{C}} \Rightarrow G F$ and counit $\varepsilon : F G \Rightarrow \mathrm{Id}{\mathcal{D}}$, satisfying the triangle identities

Two facts make adjunctions a working tool:

• Adjoints are unique up to unique natural isomorphism: a functor has at most one right adjoint.
• Right adjoints preserve limits and left adjoints preserve colimits. For instance, the forgetful functor $\mathbf{Grp} \to \mathbf{Set}$ preserves products, and $- \times A$ preserves coproducts in any CCC (so $(B + C) \times A \cong B \times A + C \times A$: distributivity comes for free).

Lawvere’s observation that the quantifiers are adjoints to substitution (1969) is the bridge from adjunctions to logic and to the semantics of dependent types.

Monads

Definition. A monad on $\mathcal{C}$ is an endofunctor $T : \mathcal{C} \to \mathcal{C}$ with natural transformations $\eta : \mathrm{Id} \Rightarrow T$ (unit) and $\mu : T T \Rightarrow T$ (multiplication) such that

These are the associativity and unit laws of a monoid, stated in the category of endofunctors with composition as the tensor product; hence the slogan “a monad is a monoid in the category of endofunctors.” A comonad is the dual (a counit $T \Rightarrow \mathrm{Id}$ and comultiplication $T \Rightarrow TT$).

Monads and adjunctions

Every adjunction $F \dashv G$ yields a monad $T = G F$ with unit $\eta$ and multiplication $\mu = G \varepsilon F$. Conversely, every monad arises from an adjunction, and there are two canonical choices: the Kleisli category $\mathcal{C}_T$ (the initial one) and the Eilenberg-Moore category $\mathcal{C}^T$ of $T$-algebras (the terminal one).

flowchart LR
    ADJ["Adjunction F -| G"] -->|"T = GF, mu = G epsilon F"| MON["Monad (T, eta, mu)"]
    MON --> KL["Kleisli category C_T<br/>objects of C, arrows A -> T B"]
    MON --> EM["Eilenberg-Moore category C^T<br/>T-algebras T X -> X"]
    KL -->|"initial resolution"| ADJ2["Adjunctions inducing T"]
    EM -->|"terminal resolution"| ADJ2

The Kleisli category is the one programmers use: its morphisms $A \to B$ are “effectful functions” $A \to T(B)$, composed by

with $\eta_A$ as identity. The monad laws are exactly the statement that this is a category. Algebras in the Eilenberg-Moore sense recover familiar structure: the algebras of the free-monoid (list) monad on Set are monoids, and the algebras of the free-group monad are groups.

Monads in functional programming

Moggi (1991) proposed monads as a uniform semantics for computational effects; Wadler popularized them as a programming technique, and Haskell adopted them for I/O. Since GHC 7.10 (the Applicative-Monad Proposal), the standard class hierarchy is Functor ⊂ Applicative ⊂ Monad:

class Applicative m => Monad m where
  (>>=)  :: m a -> (a -> m b) -> m b      -- bind
  return :: a -> m a                       -- eta; defaults to pure
  return = pure

join :: Monad m => m (m a) -> m a          -- mu
join mma = mma >>= id

(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c   -- Kleisli composition
f >=> g = \x -> f x >>= g

-- The Maybe monad (as in base): failure short-circuits
instance Monad Maybe where
  Nothing >>= _ = Nothing
  Just x  >>= f = f x

In Kleisli form the monad laws read as the category laws: return >=> f == f, f >=> return == f, and (f >=> g) >=> h == f >=> (g >=> h).

Beyond monads. Monads compose poorly in general, which led to monad transformers (StateT, ExceptT) and, more recently, to algebraic effects and handlers (Plotkin and Power; Plotkin and Pretnar), where effects are described by operations and equations and interpreted by handlers. Effect handlers are now in mainstream use: OCaml 5.0 (2022) added native effect handlers to the runtime, and languages such as Koka and Unison are built around effect systems. Applicative functors (lax monoidal functors) and arrows are weaker structures that permit more static analysis than monads.

The Lambda Calculus and Type Systems

Untyped lambda calculus

Church’s lambda calculus has three term formers:

(variable, abstraction, application). Terms are identified up to renaming of bound variables ($\alpha$-equivalence), and computation is $\beta$-reduction,

where substitution must avoid capturing free variables of $u$. The optional $\eta$-rule $\lambda x.\, t\, x \to t$ (for $x$ not free in $t$) expresses function extensionality.

Key facts:

• Church-Rosser (confluence). If $t \to^{} u_1$ and $t \to^{} u_2$ then some $v$ has $u_1 \to^{} v$ and $u_2 \to^{} v$. Normal forms, when they exist, are unique.
• Turing completeness. Natural numbers can be encoded (Church numerals $\bar n = \lambda f.\,\lambda x.\, f^n\, x$), and general recursion is available through fixed-point combinators such as $Y = \lambda f.\,(\lambda x.\, f\,(x\,x))\,(\lambda x.\, f\,(x\,x))$.
• Non-termination. $\Omega = (\lambda x.\, x\,x)(\lambda x.\, x\,x)$ reduces only to itself.
• Reduction strategies. Normal-order (leftmost-outermost) reduction finds a normal form whenever one exists; call-by-value and call-by-need (lazy evaluation) are the strategies real languages implement.

Simply typed lambda calculus

Types are built from base types and the arrow:

A typing judgment $\Gamma \vdash t : \tau$ reads “in context $\Gamma$, term $t$ has type $\tau$.” The simply typed lambda calculus (STLC) has three rules:

Its metatheory is the template for every later system:

• Subject reduction (preservation): if $\Gamma \vdash t : \tau$ and $t \to_\beta t’$ then $\Gamma \vdash t’ : \tau$.
• Progress: a closed well-typed term is either a value or can take a step. Together these give type safety (“well-typed programs do not go wrong,” Milner 1978).
• Strong normalization: every reduction sequence from a well-typed term terminates (Tait’s method of reducibility candidates). $\Omega$ has no type. Consequently STLC is not Turing-complete, and typed languages recover general recursion by adding a fixed-point operator, at the cost of logical consistency.

Polymorphism

Hindley-Milner (Hindley 1969; Milner 1978; Damas and Milner 1982) adds let-polymorphism: type schemes $\forall \alpha.\, \tau$ may be introduced only at let bindings, and quantifiers appear only at the outermost level. In exchange, type inference is decidable and every typable term has a principal type, computed by Algorithm W using unification. Hindley-Milner is the core of the ML family, OCaml, F#, and Haskell 98 (Haskell adds type classes; modern GHC extends it considerably).

System F (Girard 1972; Reynolds 1974) allows quantification anywhere, with explicit type abstraction $\Lambda \alpha.\, t$ and application $t\,[\tau]$. It is still strongly normalizing and is expressive enough to encode natural numbers, lists, and products by their elimination principles (for example $\mathrm{Nat} = \forall \alpha.\,(\alpha \to \alpha) \to \alpha \to \alpha$). However, type inference for full System F is undecidable (Wells, 1994), so practical languages require annotations for higher-rank types. Parametricity (Reynolds’ abstraction theorem) says polymorphic terms act uniformly on all types; it is the source of the “free theorems” used above for natural transformations.

The lambda cube

Barendregt’s lambda cube (1991) organizes typed calculi by which dependencies between terms and types they permit. Starting from STLC ($\lambda{\to}$) at the origin, each axis adds one kind of abstraction.

Adding inductive types and a hierarchy of universes to $\lambda C$ gives the Calculus of Inductive Constructions (CIC), the kernel theory of Rocq and, in a variant, Lean.

The Curry-Howard Correspondence

Curry (1934, for combinators) and Howard (1969, for natural deduction) observed that the typing rules of the lambda calculus are the inference rules of intuitionistic natural deduction with the terms erased. The correspondence identifies:

• propositions with types and proofs with terms: a closed term of type $A$ is a proof of $A$;
• introduction and elimination rules with constructors and destructors: $\to$I is $\lambda$-abstraction and $\to$E (modus ponens) is application;
• proof normalization (Prawitz’s detour elimination) with $\beta$-reduction. Strong normalization of STLC is the computational content of the consistency of intuitionistic propositional logic: a closed normal term of type $\bot$ cannot exist.

Example. The proposition $A \Rightarrow (B \Rightarrow A)$ is proved by the K combinator, and $(A \Rightarrow B \Rightarrow C) \Rightarrow (A \Rightarrow B) \Rightarrow A \Rightarrow C$ by the S combinator. Type-checking these definitions is checking the proofs:

k :: a -> b -> a
k x _ = x

s :: (a -> b -> c) -> (a -> b) -> a -> c
s f g x = f x (g x)

By contrast, Peirce’s law $((A \Rightarrow B) \Rightarrow A) \Rightarrow A$ is classically valid but has no total inhabitant of type ((a -> b) -> a) -> a in Haskell or STLC.

Curry-Howard-Lambek. Lambek extended the correspondence to categories: the simply typed lambda calculus with products (equivalently, the ${\top, \land, \Rightarrow}$ fragment of intuitionistic logic) is the internal language of cartesian closed categories. Adding coproducts and an initial object gives bicartesian closed categories and the full intuitionistic propositional calculus. Adding dependent types and quantifiers leads to locally cartesian closed categories and, with a subobject classifier, to toposes, whose internal logic is intuitionistic higher-order logic.

Extensions of the correspondence

The correspondence is a pattern rather than a single theorem; many logics have a matching computational system.

Affine and linear type systems have practical descendants: Rust’s ownership discipline is affine in spirit (values are used at most once unless copied), and quantitative type theory (Atkey 2018) underlies the multiplicity annotations of Idris 2.

Constructive logic

Curry-Howard is a correspondence with intuitionistic logic. A proof of $A \lor B$ must say which disjunct holds, and a proof of $\exists x.\, P(x)$ must supply a witness; this is exactly the data carried by values of sum and dependent-pair types. The law of excluded middle $A \lor \neg A$ and double-negation elimination $\neg\neg A \Rightarrow A$ (where $\neg A$ abbreviates $A \Rightarrow \bot$) are not provable, because no program can decide an arbitrary proposition. Classical reasoning is still available in two ways: by adding excluded middle as an axiom (proofs then lose some computational content, as in Lean’s Classical.em), or by interpreting classical proofs via control operators or double-negation translations (Gödel-Gentzen), which recover a computational reading.

Dependent Type Theory

Martin-Löf type theory (MLTT, 1971-1984) allows types to depend on terms. This is what is needed to state mathematics inside the type system: a type such as “vectors of length $n$” is indexed by the natural number $n$, and a proposition such as “$n$ is prime” is a type depending on $n$.

Pi and Sigma types

• The dependent function type $\prod_{x:A} B(x)$ contains functions whose result type depends on the argument. Read logically, it is $\forall x : A.\, B(x)$.
• The dependent pair type $\sum_{x:A} B(x)$ contains pairs of a witness $a$ and evidence $b : B(a)$. Read logically, it is $\exists x : A.\, B(x)$, in its strong constructive form.
• When $B$ does not depend on $x$, these reduce to $A \to B$ and $A \times B$.

Categorically, $\Sigma$ and $\Pi$ are the left and right adjoints to substitution (pullback) along a projection, which is the Lawvere adjunction from the adjunctions table. Models of dependent type theory are accordingly locally cartesian closed categories (Seely 1984, with coherence corrections by Hofmann and others).

Inductive families

Dependent type theories add inductive types (natural numbers, lists, trees) and inductive families indexed by values. The type of length-indexed vectors in Lean 4:

inductive Vec (α : Type u) : Nat → Type u where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- Total without a `nil` case: the index n + 1 rules it out.
def Vec.head : Vec α (n + 1) → α
  | .cons a _ => a

The type checker verifies that head can never be applied to an empty vector, so the property “no out-of-bounds access” is proved once by type-checking rather than tested at run time.

Universes

A type of all types, $\mathsf{Type} : \mathsf{Type}$, makes the theory inconsistent (Girard’s paradox, a type-theoretic Burali-Forti paradox). Proof assistants instead use a cumulative or non-cumulative hierarchy $\mathsf{Type}_0 : \mathsf{Type}_1 : \mathsf{Type}_2 : \cdots$, often with universe polymorphism so that definitions work at every level. Lean and Rocq also have an impredicative universe of propositions (Prop), with proof irrelevance in Lean.

Identity types and homotopy type theory

MLTT represents equality as an identity type $a =_A b$, whose inhabitants are proofs of equality, with a single constructor $\mathsf{refl}_a : a =_A a$ and an elimination rule ($J$) for reasoning by path induction. In intensional type theory (the default in Rocq, Lean, and Agda) type checking is decidable but some equalities, such as function extensionality, are not provable without an axiom. Extensional type theory adds equality reflection, which makes type checking undecidable.

Hofmann and Streicher (1994) showed that uniqueness of identity proofs is not derivable in MLTT. The later observation (Awodey-Warren, Voevodsky, around 2006) that identity types behave like paths in a space founded homotopy type theory (HoTT):

Voevodsky’s univalence axiom states that for types in a universe the canonical map $(A = B) \to (A \simeq B)$ is an equivalence: equivalent types are equal, so every construction is automatically invariant under equivalence. Together with higher inductive types (for example the circle $S^1$, generated by a point and a loop), this supports synthetic homotopy theory, as developed in the HoTT book (2013). Because univalence as an axiom blocks computation, cubical type theory (Cohen, Coquand, Huber, and Mörtberg, 2015) gives it a constructive interpretation in which univalence is a theorem; Cubical Agda implements it.

Proof Assistants

A proof assistant implements a logic or type theory so that proofs are checked by machine. Most follow the de Bruijn criterion: a small trusted kernel checks every proof, so the elaborator, tactics, and automation around it can be large and fallible without compromising soundness.

flowchart LR
    U["User: statements,<br/>tactic scripts"] --> E["Elaborator<br/>(implicit args, notation, unification)"]
    E --> T["Tactics and automation<br/>simp, grind, hammers, AI provers"]
    T --> PT["Proof term<br/>(CIC / HOL derivation)"]
    E --> PT
    PT --> K["Small trusted kernel<br/>type checker"]
    K -->|"accepted"| OK["Theorem added to environment"]
    K -->|"rejected"| ERR["Error"]

Systems

Terms and tactics

A proof can be written directly as a term or built interactively with tactics, commands such as intro, induction, rw, and simp that transform the current goal and emit a proof term behind the scenes. Because the kernel checks the resulting term, a buggy tactic can fail but cannot prove a false statement. A small Lean example:

theorem my_add_comm (m n : Nat) : m + n = n + m := by
  induction n with
  | zero      => simp
  | succ k ih => rw [Nat.add_succ, ih, Nat.succ_add]

In practice this goal is closed by omega (linear arithmetic) or grind, or by citing the library lemma Nat.add_comm; the explicit induction shows how the proof term is structured.

Landmark formalizations

Machine learning and formal proof

Formal verification gives machine-learning systems an unambiguous reward signal: a proof either type-checks or it does not. DeepMind’s AlphaProof (reinforcement learning over Lean) reached silver-medal standard on the 2024 International Mathematical Olympiad, with the method published in Nature in 2025. At the 2025 IMO, Harmonic’s Aristotle produced Lean-verified solutions to five of the six problems, a gold-medal-level score, while other systems reached gold level with unverified natural-language proofs. Current research directions include autoformalization (translating informal mathematics into formal statements), premise selection over large libraries such as mathlib, and using proof assistants to check AI-generated mathematics; see Advanced AI Mathematics.

Research Directions

• Univalent foundations and cubical methods. Making univalence and higher inductive types computational, and building libraries (agda-unimath, Cubical Agda’s library) on univalent foundations.
• Synthetic and higher category theory. Directed type theories for $(\infty, 1)$-categories, and large formalization efforts for $\infty$-categories.
• Effects and resources. Algebraic effect systems, graded and quantitative type theories, and linear types for memory safety and quantum programming (the no-cloning theorem matches linearity; see Quantum Algorithms Research).
• Applied category theory. Monoidal categories and string diagrams as a common language for quantum circuits, probabilistic programming (Markov categories), databases, and open systems.
• Mechanized mathematics at scale. Library engineering for mathlib-sized developments, proof repair, and AI-assisted formalization.

See Also

• Automata and Formal Languages: the other classical model of computation, and decidability
• Computational Complexity Theory: resource bounds on computation; the complexity of type inference and proof search
• Distributed Systems Theory: formal specification and verification with temporal logic and TLA+
• Quantum Algorithms Research: monoidal categories and linear types as semantics for quantum computation
• Advanced AI Mathematics: learning theory and AI-assisted theorem proving
• Mathematical Reference: notation and quick reference

References

1. Mac Lane, S. (1998). Categories for the Working Mathematician (2nd ed.). Springer.
2. Awodey, S. (2010). Category Theory (2nd ed.). Oxford University Press.
3. Riehl, E. (2016). Category Theory in Context. Dover.
4. Lambek, J., & Scott, P. J. (1986). Introduction to Higher-Order Categorical Logic. Cambridge University Press.
5. Pierce, B. C. (2002). Types and Programming Languages. MIT Press.
6. Girard, J.-Y., Lafont, Y., & Taylor, P. (1989). Proofs and Types. Cambridge University Press.
7. Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism. Elsevier.
8. Moggi, E. (1991). “Notions of computation and monads.” Information and Computation 93(1).
9. Wadler, P. (1989). “Theorems for free!” FPCA.
10. Martin-Löf, P. (1984). Intuitionistic Type Theory. Bibliopolis.
11. The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.
12. Barendregt, H. (1991). “Introduction to generalized type systems.” Journal of Functional Programming 1(2).
13. The mathlib Community (2020). “The Lean mathematical library.” CPP 2020.