Type theory began as Russell's fix for a paradox and now runs proof software
Imagine a collection of every set that fails to include itself: it ends up both belonging to itself and not. Bertrand Russell's answer to that paradox was a hierarchy of types, and a century later the same idea underpins proof assistants such as Lean and Rocq.
A type works much like a data type in programming, telling you what sort of object an expression denotes and what you are allowed to do with it. Between 1902 and 1908 Russell tried several remedies, settling on a ramified theory of types plus an axiom of reducibility, which appeared in Principia Mathematica, written with Whitehead and published in 1910, 1912 and 1913. Every mathematical object was assigned a level and built only from lower levels, so nothing could be defined in terms of itself.
Alonzo Church brought types to his lambda calculus, and his simply typed version escaped the Kleene–Rosser paradox that had plagued the untyped original; he showed it could serve as a foundation for mathematics, a system known as higher-order logic. Today type theory usually means a typed system built on lambda calculus. Per Martin-Löf's intuitionistic type theory was designed as a foundation for constructive mathematics, while Thierry Coquand's calculus of constructions became the base of several proof assistants.
Automath, the first computer proof assistant, already used types to encode mathematics. Now Rocq, formerly Coq, runs on the calculus of inductive constructions, Lean on dependent type theory, and Agda, both a programming language and a proof assistant, on Luo's Unified Theory of dependent Types. Mizar, by contrast, supports only set theory, and Isabelle handles ZFC alongside type theories. Any static program analysis, including the type checking inside a compiler, connects back to the field.
Some type theories are offered as rivals to set theory as the foundation of mathematics. Category theorists, uneasy with Zermelo–Fraenkel set theory, had already proposed Lawvere's Elementary Theory of the Category of Sets, and homotopy type theory carries that line forward by linking dependent types, especially the identity type, with homotopy in algebraic topology.
Source: Type theory
