1879 to 1913: Frege and Russell🔗

Gottlob Frege's Begriffsschrift of 1879 gave the first system in which proofs themselves were objects to be manipulated. That work is pure logic, and it survives. Frege then derived arithmetic from it in the Grundgesetze der Arithmetik (1893, 1903), using one further axiom: concepts with the same instances have the same extension. Bertrand Russell's letter of 1902 showed that this axiom is inconsistent. The set R = \{x : x \notin x\} is a member of itself exactly if it is not. The letter reached Frege while the second volume was in press.

Russell's set is impredicative: it is defined by quantifying over a collection that contains it. The condition ranges over all sets, and R would be one of them. Both repairs below attack that, and the word returns in Why Prop is special.

Two answers appeared in 1908, and both are still in use. They differ in what they restrict.

Zermelo replaced unrestricted comprehension, which forms \{x : \varphi(x)\} for any property, by separation, which forms only \{x \in A : \varphi(x)\} out of a set A already given. Then R is never formed, and Russell's argument turns into a theorem instead of a contradiction: there is no set of all sets. That x ∈ x holds for no set is a later and separate axiom, foundation.

Russell stratified the language itself, so that x ∈ x is not false but ungrammatical. Well-formedness is then a question about syntax, settled before any question of truth arises.

However, Russell's ban was wider than the paradox. It forbids every definition that quantifies over a totality containing the object being defined, and ordinary mathematics is full of those. The supremum of a bounded set of reals is defined by quantifying over reals, so under the ban it is not itself a real number, and analysis stops. Russell recovered it by adding an axiom, reducibility, which grants that every forbidden definition agrees with a permitted one — an axiom that returns most of what the ban had taken. Lean draws the line differently for propositions and for data: definitions that quantify over all propositions are allowed in Prop, but not over all types in Type; see Why Prop is special.

Mathematics went with Zermelo, proof assistants with Russell (Where types come from).

Whitehead and Russell spent Principia Mathematica rebuilding the rest; their proof that 1 + 1 = 2 arrives in the second volume with the note that the above proposition is occasionally useful. Done by hand, formalization is unbearable, and for most of a century little came of it.

1917 to 1931: Hilbert's programme, and Gödel🔗

David Hilbert turned formalization into a programme, pressing for it from a lecture of 1917, Axiomatisches Denken, onwards. The conviction behind it is older. At the Paris congress of 1900 he had said that in mathematics there is no ignorabimus (we shall not know): Every well-posed mathematical question can in principle be settled.

Write mathematics in a fixed formal language, fix the rules of inference, and a proof becomes a finite string of symbols. Whether it follows the rules is then a question about symbols, answerable without knowing what they mean. Three questions about a set of axioms can then be asked precisely, and Hilbert wanted all three answered yes.

• Consistent. No contradiction follows from the axioms. Hilbert wanted this proved by finitary means.

• Complete. For every statement, either it or its negation follows.

• Decidable. A procedure settles, for every statement, which of the two it is.

Gödel's two theorems need one more word. A model of a set of axioms is a concrete structure in which all of them hold. The group axioms have many models: the integers under addition, the invertible 2 \times 2 matrices, the symmetries of a square. A statement that follows from the axioms holds in every model. Commutativity x \cdot y = y \cdot x holds in the first model and fails in the other two, so it does not follow from the group axioms.

Kurt Gödel settled the first two questions, in opposite directions. His thesis of 1929 proved first-order logic complete: a formula that holds in every model is derivable from the axioms. First-order is the restriction that quantifiers range over the elements of a domain, never over its subsets, relations or functions. \forall x\, \exists y\, (x \cdot y = e) is first-order; every bounded set of reals has a supremum is not, because it quantifies over sets of reals. Logic itself is therefore not the obstacle.

The incompleteness theorems of 1931 end the programme. No consistent system that contains arithmetic and whose axioms a machine can list proves every true statement about the natural numbers, and none proves its own consistency. The formalization itself survived, and it is what proof assistants rest on. Gödel's proof takes it literally: he encodes formulas and proofs as natural numbers and computes with them, the first use of proofs as data. The argument is Cantor's diagonal argument, carried over from the reals to proofs. Turing used it again five years later.

The word complete does two jobs here. A logic is complete when every formula that holds in all models is derivable; a theory is complete when it decides every statement, which is the sense of Hilbert's list above. The two theorems are about the two different things.

They do not conflict. The axioms of arithmetic have models other than \mathbb{N}. These nonstandard models contain a copy of 0, 1, 2, \dots and, beyond it, further elements larger than every one of these. Recall that Gödel numbers proofs: every proof is a finite string of symbols, and he assigns to each such string a natural number, its code. The sentence he builds in 1931 says, in effect, I am not provable. As a statement about numbers it reads: no natural number is the code of a proof of this sentence. In \mathbb{N} it is true. In some nonstandard model it is false: there, one of the extra elements satisfies the formula is the code of a proof of this sentence, although no actual proof has it as its code. So the sentence does not hold in every model, and the theorem of 1929 promises nothing for it. Such a model must exist, by the theorem of 1929: since the sentence is not provable, adding its negation to the axioms is consistent, and a consistent first-order theory has a model.

1936: the Entscheidungsproblem🔗

The third question was left. Hilbert and Wilhelm Ackermann put it in print in 1928, in Grundzüge der theoretischen Logik: is there a procedure that decides, for an arbitrary formula of first-order logic, whether it is provable? This is the Entscheidungsproblem. Alonzo Church and Alan Turing answered it in 1936, independently and negatively. There is no such procedure.

Both had to say first what a procedure is, and each built a formal definition of computation to do it. Turing's is the machine that carries his name: a tape divided into cells, a head that reads one cell, writes and moves one step, and a finite table of instructions. The paper does not say how such a machine would be built; it is there to be reasoned about, not constructed. Church's is the lambda calculus, which we will use in this course.

A calculus is a formal language together with rules for calculating with its expressions. The lambda calculus has terms for functions and a single rule. The term \lambda x.\, x + 1 denotes the function sending x to x + 1, the term f\, a denotes f applied to a, and the rule is substitution: (\lambda x.\, x + 1)\, 3 \;\rightsquigarrow\; 3 + 1. This step is called β-reduction; it is one of the reduction rules of Lean in the next chapter. Numbers, pairs and recursion are not built in; they are written as lambda terms. This is why the calculus can serve as a definition of computation, and not only as a way of writing functions. Turing proved in an appendix to his paper that his machines and Church's terms compute the same functions. He went to Princeton the following year and took his doctorate under Church. That the two definitions agree is a theorem. That either of them captures what we informally call computable cannot be a theorem, because the informal notion has no definition to prove anything from. This claim is the Church-Turing thesis. It is supported by evidence: every other definition proposed since has turned out to compute the same functions.

Lean is this calculus with types on top. The Lean spelling of \lambda x.\, x+1 is fun x => x + 1, and the kernel computes by substituting. The proof rfl below asks it to check that both sides reduce to the same term:

The step from a calculus of functions to a calculus of proofs is the Curry-Howard correspondence: a proposition is a type, a proof is a term of that type, and checking a proof is type-checking a program. Haskell Curry saw the pattern for implication in the 1930s; de Bruijn, William Howard and Hans Läuchli extended it to the quantifiers in the 1960s. It is the reason theorem and def are the same construct in Lean.

Three questions about proofs have three different answers, and a proof assistant is built on the difference.

1. Does this text prove that statement? Decidable, and cheap. This is what Lean's kernel does, and the whole trust of the system rests on it.

2. Find a proof of this statement. Semi-decidable, and question 1 is the whole reason: proof texts are finite objects, so one can enumerate them and check each. The search ends when a proof exists and runs forever when none does, which is why exact? and grind come with a time limit. Gödel's completeness theorem is not what makes this work, and here it would not be available. It says that derivable and true in every model coincide for first-order logic; Lean's logic is higher-order, and by the theorem of 1931 it leaves true statements about \mathbb{N} unproved. The search looks for proofs, not for truths.

3. Decide whether this statement is provable — always, and with yes or no. Undecidable, by Church and Turing.

Rows 2 and 3 ask the same question and differ only in what is demanded, which is the whole of the third column. Semi-decidable says the second column is filled; undecidable says the third is not. The two words do not conflict. The gap is one-sided, and it is what you see when grind hangs. It cannot tell you that there is nothing to find, only that it has not found anything yet. The second row is also where automated proof search, begun in the 1950s (below), comes back: omega, grind and bv_decide search, and in the last case an external SAT solver does, but the result is handed to the kernel as something to check. The search may be unreliable in any way it likes; the check is small and fixed.

So the human writes the proof and the machine checks it. That division of labour is a theorem of 1936, not a property of today's software.

1967: Automath🔗

Nicolaas Govert de Bruijn started Automath at Eindhoven in 1967 and published it in 1968, the first language in which a machine checked proofs. The move is a retreat from the second question to the first. The field that follows is named after what the human keeps doing, interactive theorem proving. Its foundation is a typed lambda calculus with dependent types, that is, types that may mention terms, as Vec α n (lists of length n) mentions n. It was the first system in which a proof is a term and checking it is type-checking, the Curry-Howard correspondence; de Bruijn found that correspondence himself, not knowing Howard's work. In 1977 L. S. van Benthem Jutting pushed Landau's Grundlagen der Analysis through it, the first mathematics book verified end to end.

1972 to 1991: Mizar, LCF, HOL, Isabelle, Coq🔗

Automath left two problems open. Its proofs were written step by step, with no help from the machine, and they were unreadable to mathematicians. Four lines come out of the following twenty years, and each one starts from a problem the earlier systems had.

• Mizar, Andrzej Trybulec, 1973. Problem: Automath texts are unreadable. Answer: a formal language meant to be read like mathematical prose, over the foundation mathematicians already use, set theory in first-order logic. Its library has been growing for fifty years. Still missing: the user cannot add automation of their own; the checker is fixed.

• LCF, Robin Milner, Stanford 1972 and Edinburgh 1975. Problem: automation is a large program, and a bug in it could produce false theorems. Answer: thm is an abstract data type, and the only functions that produce a value of that type are the inference rules. Tactics may then be written by anyone, in the language ML that was invented for this, without being trusted. Still missing: the logic of LCF was made for reasoning about programs, not for mathematics in general.

• HOL, Mike Gordon, from the mid-1980s. Problem: the logic. Answer: LCF with simple type theory, Church's higher-order logic of 1940. It quantifies over functions and sets, which is enough for most of mathematics. Isabelle follows in 1986 (Lawrence Paulson), Isabelle/HOL in 1991 (Tobias Nipkow). Still missing: types cannot depend on terms, so Vec α n cannot be written.

• Coq, from 1989. Problem: dependent types and tactics had not yet met. Answer: the Calculus of Constructions (Thierry Coquand and Gérard Huet), a dependent type theory in the Automath line, with LCF-style tactics on top. Propositions, proofs and programs are written in one language. Still missing: ℕ is not built in. It must be encoded by functions, and for that encoding induction cannot be proved. Answer, from the early 1990s: the Calculus of Inductive Constructions (Coquand and Christine Paulin-Mohring), where inductive types such as ℕ are primitive and come with their recursor. That is the foundation Lean also uses.

A proof assistant is a large program, and large programs have bugs. So the question is which part of it must be correct for an accepted theorem to be actually proved. The LCF and the Automath line answer it differently. In the LCF line only the theorem is kept, not the proof. A bug in a tactic still cannot produce a false theorem, because only the inference rules can produce a value of type thm. So only the inference rules must be correct. In the Automath line the system writes down a proof term, which a small, separate checker reads afterwards. Then only the checker must be correct; a system meeting that condition is said to satisfy the de Bruijn criterion. Lean is in the second line: a Lean proof is a term, and the kernel rechecks it no matter which tactic produced it.

Almost nothing here died. Mizar has run for fifty years, and Isabelle, Rocq and the HOL family are maintained today; only Automath and LCF stopped, and each left its architecture to its successors. The field accumulates rather than replaces, and the reason is that a library cannot be moved: seL4 stays in Isabelle, the four colour theorem stays in Rocq, and nobody will do either again.

2013: Lean🔗

Leonardo de Moura started Lean at Microsoft Research in 2013. Lean 4, a redesign rather than a new version, arrived in 2021, and is written in Lean itself. Its foundation is the Calculus of Inductive Constructions, which puts it in the Automath line. Kevin Buzzard has argued for Lean among mathematicians since 2018. Where development sits now is Current state of Lean, after the record.

The three systems today🔗

The two systems Lean is usually compared with differ from it in their foundations, not in style.

Lean and Rocq are close relatives. Both rest on a dependent type theory in which a proof is a term and checking a proof is type-checking; both have an impredicative, proof-irrelevant universe Prop of propositions sitting under a predicative hierarchy of data types. Lean differs in four points that return later in these notes: proof irrelevance holds definitionally, quotient types are primitive rather than built from setoids, there is no universe cumulativity, and classical reasoning enters through an axiom (Classical.choice). Rocq's roots are in program verification — the CompCert C compiler and the Feit-Thompson theorem are Rocq developments — and it extracts verified programs to OCaml or Haskell.

Isabelle/HOL uses simple type theory: types are built from base types and arrows, and there are no dependent types. That logic is weak enough to automate well, and Isabelle's automation is the strongest of the three. Sledgehammer hands a goal to several external provers at once and reconstructs what they find as a proof Isabelle can check; much of what Lean's grind does, Isabelle has done for twenty years. Isabelle is also a framework: HOL is one object logic among several over the intuitionistic meta-logic Isabelle/Pure. Its largest development is seL4, an operating-system microkernel verified down to its C implementation.

How the libraries are organized matters more day to day than the foundations.

• Mathlib is one repository, compiled as a unit. Maintainers review every change, and CI keeps it building against the current Lean. There are no stable releases: Mathlib follows Lean, and your project follows Mathlib. Results combine without extra work, because all structures live in one hierarchy, built from class and instance (see the chapters on typeclasses and the algebraic hierarchy).

• Rocq has no such centre. Its standard library is small, and the mathematics lives in independent packages — MathComp, out of the Feit-Thompson formalization, Coquelicot and MathComp-Analysis for analysis, and others — distributed through opam, with the Rocq Platform bundling a tested combination. Packages evolve at their own pace, which is comfortable with one dependency and awkward with two that disagree.

• Isabelle sits in between. The Archive of Formal Proofs holds refereed, self-contained entries, released in lockstep with Isabelle. Entries may depend on one another but are never merged into one library; the archive is cited like a journal.

We use Lean because Mathlib exists: the exercises start with import Mathlib and have the real numbers, measure theory and topology already there.

1976: the four colour theorem🔗

Kenneth Appel and Wolfgang Haken proved the four colour theorem. Their argument reduced the problem to a long list of configurations and then checked that list by computer. No human has ever read that part, and for two decades the community argued about whether it counted as a proof at all.

In 2005 Georges Gonthier formalized the whole thing in Coq, case analysis included. The two events separate the distinction this course rests on: a proof found by computer is not a proof checked by computer.

1998: the Kepler conjecture🔗

Thomas Hales announced a proof of the Kepler conjecture: no packing of equal spheres in space is denser than the way a greengrocer stacks oranges.

Twelve referees worked on it for four years and reported that they were ninety-nine percent certain, and could do no better. The Annals of Mathematics published it with that caveat. Hales started the Flyspeck project, which delivered a complete formal proof in HOL Light and Isabelle in 2014: about twenty human work-years and some 500 000 lines of proof script (Hales, 2026)Thomas Hales, 2026. “What Mathematicians Should Know About the Lean Theorem Prover: Questions of Reliability and AI”. In Guest post on Terence Tao's blog, 9 October 2026.. This episode is not about computers: peer review had met a proof it could not certify, and more effort would not have helped.

2013: Voevodsky🔗

In 1989 Vladimir Voevodsky and Mikhail Kapranov published a theorem identifying higher groupoids with homotopy types. In October 1998 Carlos Simpson posted an argument implying that it could not be true. Voevodsky went on believing his own theorem until the autumn of 2013, when he accepted Simpson's argument and found the error in his own. The theorem is false. The rigid, strictly associative kind of higher groupoid it uses cannot produce the two-sphere, and Dimitri Ara showed in 2012 that among simply connected spaces it produces exactly the products of Eilenberg-MacLane spaces — a thin slice of what had been claimed.

His account is about people, not machines. Simpson had a counterexample but could not say which step was wrong, so it stayed unclear who had erred. Mathematics runs, in Voevodsky's words, on a complex system of mutual trust based on reputations, and both authors had one. The doubt made the theorem unused without settling it, for fifteen years. A second mistake, in a lemma of his own from 1992, stood in print until a listener checking his lectures found it in 1999; several seminars had read the paper by then. A hard technical argument by a trusted author, he concluded, is hardly ever checked in detail.

Voevodsky received the Fields Medal in 2002, and spent the rest of his career on foundations designed so that a machine could check such arguments — not the ones Mathlib rests on, and not this course's subject (other type theories). This course takes the diagnosis, not the cure. His own account is short. He died in 2017.

2019: perfectoid spaces🔗

By Buzzard, Commelin and Massot (project page). They formalized a definition rather than a theorem: Scholze's perfectoid spaces of 2012. Whether an object of that complexity could be stated at all in a proof assistant was open, and stating is a different problem from proving. Lean's reputation among mathematicians dates from this project.

2020: the Liquid Tensor Experiment🔗

In December 2020 Peter Scholze posed a challenge on Kevin Buzzard's blog: a theorem in condensed mathematics whose proof he was not sure of. A Fields medallist, publicly unsure of his own argument, asking a machine to check it. The Liquid Tensor Experiment, led by Johan Commelin, finished in July 2022. Condensed mathematics rebuilds topology on profinite sets rather than on open covers. The request came from a working mathematician at the centre of his subject, not from logicians or computer scientists. That is what had changed.

Buzzard's plenary lecture at the ICM in 2022 marks the point where formalization stopped being a curiosity.

2022: sphere eversion🔗

By Massot, van Doorn and Nash (project page): Gromov's h-principle, and with it the fact that a sphere can be turned inside out without tearing or creasing. For closed curves in the plane no such thing is possible: a regular homotopy cannot change the turning number, and everting a circle would send +1 to -1. In three dimensions that obstruction vanishes. Formalizing this meant differential topology rather than algebra, so the project built a usable differential-geometry API first and proved the theorem afterwards. That order is the ordinary shape of formalization work, and it is why Mathlib matters more than any single theorem in it.

2023: the polynomial Freiman-Ruzsa conjecture🔗

By Gowers, Green, Manners and Tao (project page), formalized under Tao's direction in about three weeks — before the paper had been refereed. It says that a set whose sumset is barely larger than itself must be structured.

The method carried further than the theorem. A blueprint cuts a formalization into independent pieces with stated interfaces, so volunteers can work in parallel without talking to each other. Formalization stopped being a job for one team over years.

2024 to 2025: the Equational Theories Project🔗

Led by Tao (project page): all 22 028 942 implications between 4 694 equational laws on magmas settled, with new constructions found on the way. The difficulty is not depth but bookkeeping, on a scale that needs a machine.

The laws are numbered. Equation 3 is x = x \diamond x, Equation 4 is x = x \diamond y. Proving an implication can be a single substitution; refuting one means building a magma.

The tactic decide checks both statements by trying every element of Bool. That is one entry. The project settled 22 028 942 of them.

2026: the summer of soundness bugs🔗

In July and August 2026, several bugs were found in the Lean kernel itself, each of which allowed a proof of False. From False, everything follows. All were repaired within days, and Mathlib was rechecked with the repaired kernel.