Introduction🔗

What formalizing means, why anyone does it, how the field got here, and how this course is run.

What formalizing means🔗

To formalize a proof is to write it in a language precise enough that a computer can check every step. The machine does not look for the proof. It reads the one you give it and confirms that each step follows from the axioms and from what came before. Anything left out is refused.

Finding a proof is not checking one. In 1976 a computer checked a long list of cases in the four colour theorem. The argument around that list was ordinary mathematics on paper, and nothing checked it.

Autoformalizing goes the other way. Formalizing starts from a proof and ends in a formal text. Autoformalizing starts from informal mathematics -- a statement, a paper -- and has a machine produce that text. Both end at the same place, a text the kernel accepts. The program that writes a proof may be unreliable in any way it likes; the program that checks it is small and fixed.

This course is about the first direction. You will write the proofs.

Why formalize?🔗

Until recently, formalizing a serious theorem took a team and several years. That is no longer so, and the change is recent enough to date precisely.

February 2026. The sphere packing theorem in dimension 8 was finished by an autoformalizer in five days. A human project had been working on it since 2024. It is the first of these results and the clearest: the mathematics was settled, so only the formalizing was left. Maryna Viazovska proved the dimension-8 case in 2016 and received the Fields Medal for it, which closes a thread that opens with Kepler four hundred years earlier.
4 September 2026. Anthropic announced the first complete computer-checked proof of Fermat's Last Theorem, produced by Claude over eleven days: roughly 13 million lines of Lean and some 29 500 intermediate theorems, following a simplified version of Wiles's 1995 proof and building on Mathlib. Kevin Buzzard, who has led the community formalization effort since 2024 on a five-year grant, reviewed it and confirmed that it proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics. That confirmation is itself machine-checkable, by #print axioms (Appendix).
8 September 2026. OpenAI announced a proof, with a Lean formalization, that a smooth three-dimensional fluid obeying the Navier-Stokes equations under a smooth external force can develop a singularity in finite time. This is not the Millennium Prize problem, which concerns the unforced equation, and the prize is unclaimed. It was followed by a public argument about credit, and about treating open problems as benchmarks.
6 October 2026. OpenAI published a catalogue of results from an unreleased internal model -- at the time of writing 719 manuscripts grouped into 372 families, of which about 42 % of the top-line results carry a Lean formalization. Each result took, on average, about three hours of the model's thinking time; roughly 4 000 problems were posed in all.
7 October 2026. One day later, three of those manuscripts were withdrawn: a sign error invalidated an argument in one, and two further papers depended on it. Fourteen more were revised. None of the withdrawn papers had a Lean proof.

Claude — The two systems behind the September 2026 announcements. Both delivered Lean files with their proofs

ChatGPT — The two systems behind the September 2026 announcements. Both delivered Lean files with their proofs

Those last two dates belong together. Machines now produce mathematics faster than mathematicians can referee it, and the only check that keeps up is a formal one.

A Lean proof shows that the formal statement follows from the axioms. It does not show that the statement says what the paper claims; that is a separate, human question. OpenAI's repository documents, per paper, which checks cover a main theorem and which only a supporting result. Reading a formal statement and judging what it says is most of what this course teaches.

Where the field stands🔗

Two pictures from public data. They compare Lean with Rocq (Coq until 2025) and Isabelle/HOL, the two other large proof assistants; how they differ is a question of foundations, taken up under Other theorem provers.

Line chart: new GitHub repositories per quarter for Lean, Coq/Rocq and Isabelle from 2018 to 2026, each per million new repositories overall; Lean rises from under ten to about two hundred while the others stay near ten — New GitHub repositories per quarter, per million new repositories overall

Counting per million corrects for GitHub's own growth, which was steep in 2026. One distortion is left in: the Justin Sun Prize, announced in September 2026, pays for solved problems only against a machine-verified proof, and about a fifth of that month's new Lean repositories carry a prize identifier.

Until about 2023 the three were comparable, with Coq the largest. The rise is recent, and it is not evidence that Lean is better: Isabelle's automation is still ahead in places, and Rocq has decades of verified-software work behind it. It is evidence about where people are going.

Bar chart: weekly share of arXiv mathematics papers with a Lean-checked result during 2026, rising from about 0.3 per 100 in January to between 1.5 and 2 per 100 in September — Papers on the mathematics arXiv whose results are checked in Lean, per 100 submissions

The share rises through 2026 and is still under two in a hundred. It is a share rather than a count because the denominator moved too: the mathematics arXiv received about a thousand submissions a week in January and about twice that at the end of September. Within a few years, reading and writing a formal proof will be ordinary equipment.

How it got here🔗

The idea is a century and a half old. The four episodes that made it urgent all fall in the last fifty years, and each added a different reason to want a machine to check mathematics.

Before there were machines🔗

Gottlob Frege's Begriffsschrift of 1879 gave the first system in which proofs themselves were objects to be manipulated; Bertrand Russell's letter of 1902 showed that the system was inconsistent. Whitehead and Russell spent Principia Mathematica rebuilding; 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.

David Hilbert turned the idea into a programme in the 1920s. 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. Hilbert asked for two things on top of that: a proof that the system is consistent, using finitary means only, and a procedure deciding every mathematical question.

Kurt Gödel's incompleteness theorems of 1931 removed the first. 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.

1936: what a machine cannot do🔗

Hilbert and Wilhelm Ackermann asked in 1928, in Grundzüge der theoretischen Logik, for 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 model of computation to do it. Turing's is the machine that carries his name: a tape, a finite control, one symbol at a time. Church's is the lambda calculus, and it is the one this course uses every day.

The lambda calculus is a notation for functions, and nothing else. 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 only rule of computation is substitution: (\lambda x.\, x + 1)\, 3 \;\rightsquigarrow\; 3 + 1. Numbers, pairs and recursion are not built in; they are written as lambda terms. That is what makes the calculus a model of computation and not just a notation. Turing proved in an appendix to his paper that his machines and Church's terms compute the same functions.

Lean is this notation with types on top. The Lean spelling of \lambda x.\, x+1 is fun x => x + 1, and the kernel computes by substituting:

fun x => x + 1 : ℕ → ℕ#check fun x : Nat => x + 1

example : (fun x : Nat => x + 1) 3 = 3 + 1 := rfl

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.

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.
Find a proof of this statement. Semi-decidable. Proofs can be enumerated one after another, so a search ends when a proof exists. When none exists it runs forever, which is why exact? and grind come with a time limit.
Decide whether this statement is provable. Undecidable, by Church and Turing. No procedure answers yes or no, in finite time, for every formula.

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.

The first proof assistants🔗

Nicolaas Govert de Bruijn started Automath at Eindhoven in 1967 and published it in 1968, the first language in which a machine checked proofs. Its foundation is a typed lambda calculus with dependent types -- types that may mention terms, as Vec α n mentions n -- and it was the first system to use the Curry-Howard correspondence in practice; de Bruijn found the 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.

Four lines come out of the following twenty years, and the systems of today are on them.

Mizar, Andrzej Trybulec, 1973. A formal language meant to be read like mathematical prose, over set theory. Its library has been growing for fifty years.
LCF, Robin Milner, Stanford 1972 and Edinburgh 1975. The idea there is architectural: thm is an abstract data type, and the only functions that produce a value of that type are the inference rules. Anything may then be built on top without being trusted. The language ML was invented to write it.
HOL, Mike Gordon, from the mid-1980s: LCF with simple higher-order logic in place of the original logic, used first for hardware verification. Isabelle follows in 1986 (Lawrence Paulson), Isabelle/HOL in 1991 (Tobias Nipkow).
Coq, from 1989, on the Calculus of Constructions and from the mid-1990s on the Calculus of Inductive Constructions. That is the foundation Lean also uses, and the system was renamed Rocq in 2025.

The two architectures answer the same question differently. In the LCF line nothing is kept but the theorem, and one trusts the kernel because no other code can make one. In the Automath line the system writes down a proof term, which a small, separate checker reads afterwards; 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.

1976: what a computer proof is worth🔗

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.

A map of thirty-four regions, coloured with four colours so that no two neighbours share one — Four colours suffice for any map in the plane. Georges Gonthier, who formalized the proof

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: where peer review stops🔗

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.

A pyramid of equal spheres, the face-centred cubic packing, with density pi over root 18 — The packing Kepler conjectured to be optimal in 1611, and Thomas Hales, who proved it

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. This episode is not about computers: peer review had met a proof it could not certify, and more effort would not have helped.

2013: whether the author can trust himself🔗

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.

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. He then looked for a proof assistant he could use, found none that suited his mathematics, and built the foundations for one: univalent foundations, a special year at the Institute for Advanced Study in 2012-13, and the book two dozen people wrote there in under six months. He formalized in Coq, and his foundations are not the ones Mathlib rests on: Lean 2 carried a mode for them, Lean 3 dropped it. This course takes the diagnosis, not the cure. His own account is short. He died in 2017.

2020: who is asking for it now🔗

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.

The tool is much younger than the idea🔗

Leonardo de Moura started Lean at Microsoft Research in 2013. Lean 4, a redesign rather than a new version, arrived in 2021. Development now sits with the Lean FRO, a non-profit of roughly twenty people. Kevin Buzzard has argued for Lean among mathematicians since 2018.

Landmark formalizations🔗

Between Flyspeck and 2026, each of these projects showed that something new was possible. The course material is built out of the libraries they left behind.

Perfectoid spaces, 2019🔗

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.

Kevin Buzzard, Johan Commelin and Patrick Massot

Sphere eversion, 2022🔗

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.

The polynomial Freiman-Ruzsa conjecture, 2023🔗

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.

Timothy Gowers, Ben Green, Terence Tao and Freddie Manners

Timothy Gowers, Ben Green, Terence Tao and Freddie Manners

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.

The Equational Theories Project, 2024 to 2025🔗

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.

abbrev Equation3 (a : Type) [Mul a] :=
  ∀ x : a, x = x * x

abbrev Equation4 (a : Type) [Mul a] :=
  ∀ x y : a, x = x * y

-- Equation 4 implies Equation 3: take y := x.
example (a : Type) [Mul a] (h : Equation4 a) :
    Equation3 a :=
  fun x => h x x

-- The converse fails: `and` on `Bool` is a
-- counterexample, and the machine checks it.
local instance : Mul Bool := ⟨(· && ·)⟩

example : Equation3 Bool := by⊢ Equation3 Bool decideAll goals completed! 🐙
example : ¬ Equation4 Bool := by⊢ ¬Equation4 Bool decideAll goals completed! 🐙

That is one entry. The project settled 22 028 942 of them.

Other theorem provers🔗

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

System	Foundation	Dependent types	Library
Lean 4	a variant of the Calculus of Inductive Constructions	yes	Mathlib, one repository
Rocq (until 2025 Coq)	the predicative Calculus of Cumulative Inductive Constructions	yes	many separate packages
Isabelle/HOL	simply typed higher-order logic	no	the Archive of Formal Proofs

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, types do not depend on terms, and one cannot write Vec α n for lists of length n. 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.

Other courses🔗

Natural Number Game: proofs about ℕ in the browser, nothing to install. The usual first contact with Lean, and a good use of an evening before the course starts.
Formalising Mathematics by Bhavik Mehta, after notes by Kevin Buzzard: the format of the present course follows these.
Mathematics in Lean by Jeremy Avigad and Patrick Massot: the closest thing to an official course, organized by area of mathematics.

Lean and Mathlib🔗

Lean is also a programming language; see Functional Programming in Lean.
Mathlib is a library written in Lean, collecting mathematical results. Every file in this course starts with import Mathlib, so we make no distinction between the two.
Measured on the version pinned for this course (15 September 2026): 8 529 files, 2.33 million lines, about 189 000 theorems and lemmas, about 64 000 definitions, instances and structures, by 1 031 contributors in 34 768 commits. In the thirty days before that date it received 820 commits, 27 per day. The library changes while you use it.
The interactive import map draws Mathlib as a graph of its modules; the same site serves the API documentation for every declaration. Both are worth half an hour before you need them.

Practical matters🔗

The rest of this chapter is about running the course.

Goals. The course is for mathematics students.

Interactive theorem proving. A small kernel checks every logical step of a proof, and the editor reports what remains to be proved as you write. This is not the older use of computers in mathematics, which was to work through many cases.
Mathematical content. The mathematics in the first half is deliberately easy, because explaining a proof to a computer requires understanding it first, and a proof of more than a few lines has to be planned so that the commands -- tactics -- fit together. The second half goes deeper into the mathematics.
Functional programming. Inductive types, structures, typeclasses and monads, needed both to use Lean and to read Mathlib. These are spread across the Lean and Mathematics parts rather than collected in one chapter.
Type theory. Lean rests on dependent type theory: the Curry-Howard correspondence, dependent types, the universe hierarchy, and Lean's axioms.
Mathematics in Mathlib. How the library organizes order theory, the algebraic hierarchy, filters (a single framework for limits), topology, measure theory and discrete probability. Textbooks rarely treat these from the point of view of formalization.
Proof engineering. Automation tactics, searching Mathlib, and the common pitfalls of a large formal library.

How the course is organized. Tactics and theory are interleaved rather than separated.

The first part, Lean and its type theory, introduces writing proofs and the dependent type theory underneath at the same time.
Tactics are documented alphabetically in a glossary in the Appendix. You will usually meet a tactic in a working example before reading its entry; a table at the start of Proofs in Lean lists the ones needed first.
Read in order, but on a first pass you can skip the tactics chapter and consult it when you hit a sorry.

How to use this course. The notes have six parts.

Lean and its type theory: first the language, writing proofs, the functional-programming side (pure functions, pattern matching, recursion, higher-order functions) and navigating Mathlib; then the theory -- Curry-Howard, dependent types, universes, Lean's three axioms and what the kernel adds to them, the structure / class machinery, well-foundedness and the avoidance of paradoxes.
Mathematics: propositions, proofs and sets, then how Mathlib organizes order theory, the algebraic hierarchy, filters, topology, measure theory and monadic discrete probability (PMF). Pointers into the API, not full formalizations.
Appendix: common pitfalls, the diagnostic commands (#print axioms, #find_home, #lint), a keyword reference and the glossary of tactics (a longer list is here).
Projects: five topics for the individual formalization projects in the second half, each with a description, a sketch of an implementation and references.
Bibliography: the works cited throughout, with links.
Slides: the decks used in the lecture, readable on their own.

The exercises carry the course (the Exercises folder within Leancourse). Feedback is immediate: error messages from the elaborator, and a proof-state panel showing what remains to be proved at every cursor position. Start with the first sheet; the sheets explain as they go.

The sheets cover the first half of the semester. In the second half you work on an individual project, mostly self-chosen -- an exercise from your first year, or a part of Mathlib you want to know; the Projects chapter has five worked-out suggestions.

Before the first exercise session, get Lean running on your own machine.

Hardware. Lean memory-maps all of Mathlib while it works, and every exercise sheet begins with import Mathlib. A two-line sheet therefore needs as much memory as the hardest one in the course.

Resource	Minimum	Comfortable
RAM	16 GB	32 GB
Free disk space	20 GB	20 GB
Disk	SSD	NVMe SSD

Measured on the version of Mathlib used here: compiling one sheet peaks at about 6.6 GB of resident memory, and the language server behind vscode sits at roughly 9 GB with one file open. Most of that is memory-mapped library data, which the system can drop and read back from disk, so less memory does not break anything, it only slows everything down. With 8 GB you can work with a single file open and little else running. On a mechanical hard disk you cannot.

If your machine is below the minimum, talk to the teachers at the start of the course. A server with 128 GB of RAM is available and we can give you an account on it.

Run the git clone and lake exe cache get below at home, before the first lab session: lake exe cache get downloads several gigabytes, and twenty people doing that at once on one network is slow for all of them.

Installation of vscode.
Open vscode, hit the extensions icon (fifth from the top) on the left, and install the Lean 4 language extension.
Install git, if you do not have it: open vscode, hit the git icon (third from the top on the left), and follow the instructions.
The exercises repository. Go to where you want the course materials and run

git clone https://github.com/pfaffelh/leancourse_exercises
cd leancourse_exercises
lake exe cache get
code .

vscode opens with the course materials. (These notes are generated from a second repository, pfaffelh/leancourse, which you do not need to clone.)

Another description of the installation is here.

After code . in the leancourse_exercises folder, open Exercises/01-Logic/01-a-Propositions.lean. It works once the orange and red bars disappear and moving the cursor on the left changes the infoview on the right.

Copy the Exercises directory to MyExercises and work there. MyExercises is ignored by git, so an update never overwrites your files.
To update, run git pull in leancourse_exercises.

If the installation gives you trouble, talk to the teachers rather than spending evenings on it.

Sources🔗

The history follows three surveys, all freely available:

John Harrison, Josef Urban and Freek Wiedijk, History of Interactive Theorem Proving, in Handbook of the History of Logic 9, Elsevier 2014, 135-214. The standard account, written by three people who built the systems.
Herman Geuvers, Proof assistants: history, ideas and future, Sadhana 34 (2009), 3-25. Organized by idea rather than by year.
Lawrence Paulson, 50 years of proof assistants, 2025. The LCF line from the inside.

Where a date or a formulation above comes from one text in particular:

Alan Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the London Mathematical Society (2) 42 (1936-37), 230-265.
N. G. de Bruijn, Automath, a language for mathematics, TH-Report 68-WSK-05, Eindhoven 1968.
Robin Milner, Logic for Computable Functions, Stanford AIM-169, 1972.
Lawrence Paulson, Tobias Nipkow and Makarius Wenzel, From LCF to Isabelle/HOL, 2019.
Freek Wiedijk, The Seventeen Provers of the World, Springer LNAI 3600, 2006.
Fairouz Kamareddine, Joe Wells, Christoph Zengler and Henk Barendregt, Characteristics of de Bruijn's early proof checker Automath, Fundamenta Informaticae 185 (2022), 313-336.

Four sources are on paper or behind a paywall and are only paraphrased here: Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928), Church's two papers of 1936, Russell's letter of 1902 in van Heijenoort's From Frege to Gödel, and Curry and Feys' Combinatory Logic (1958). sources/history-of-itp.md in the repository lists all of them.

Picture credits🔗

The mathematical figures were generated by the scripts in scripts/ and may be reused freely. The photographs, here and in the slide decks, come from Wikimedia Commons and are reproduced under their own licences, unchanged except where noted:

Thomas Hales -- Slawekb, CC BY-SA 3.0, via Wikimedia Commons
Peter Scholze -- George Bergman, CC BY-SA 4.0, via Wikimedia Commons
Kevin Buzzard -- George Bergman, CC BY-SA 4.0, via Wikimedia Commons.jpg)
Leonardo de Moura -- David Monniaux, CC BY-SA 4.0, via Wikimedia Commons
Maryna Viazovska -- Petra Lein, Archives of the Mathematisches Forschungsinstitut Oberwolfach, CC BY-SA 2.0 de, via Wikimedia Commons
Timothy Gowers -- Gert-Martin Greuel, Archives of the Mathematisches Forschungsinstitut Oberwolfach, CC BY-SA 2.0 de, via Wikimedia Commons
Ben Green -- Renate Schmid, Archives of the Mathematisches Forschungsinstitut Oberwolfach, CC BY-SA 2.0 de, via Wikimedia Commons
Vladimir Voevodsky -- Renate Schmid, Archives of the Mathematisches Forschungsinstitut Oberwolfach, CC BY-SA 2.0 de, via Wikimedia Commons
Terence Tao -- Institute for Pure and Applied Mathematics, CC BY 4.0, via Wikimedia Commons
Gottlob Frege, around 1879 -- photographer unknown, public domain, via Wikimedia Commons
Bertrand Russell in 1907 -- photographer unknown, public domain, via Wikimedia Commons
David Hilbert -- photographer unknown, public domain, via Wikimedia Commons
Kurt Gödel -- photographer unknown, public domain, via Wikimedia Commons
Alan Turing in 1951 -- Elliott and Fry, public domain, via Wikimedia Commons
Nicolaas Govert de Bruijn -- Konrad Jacobs, Archives of the Mathematisches Forschungsinstitut Oberwolfach, CC BY-SA 2.0 de, cropped to head and shoulders, via Wikimedia Commons

The two product marks in this chapter -- Claude and ChatGPT -- are also from Wikimedia Commons, under CC0 and in the public domain respectively. They remain trademarks of their owners and are used here only to say which system produced which proof.

The icon in the browser tab is the L of the Lean wordmark, redrawn as a single stroke on a square in the Freiburg identity blue (#34499a). The source is static/favicon.svg.

Several people named in this chapter have no freely licensed photograph, and the pattern is not an accident: Georges Gonthier, who formalized both the four colour theorem and the Feit-Thompson theorem, Johan Commelin, who led the Liquid Tensor Experiment, Patrick Massot, Floris van Doorn and Oliver Nash, who formalized sphere eversion, and Freddie Manners, one of the four authors of the polynomial Freiman-Ruzsa theorem. Alonzo Church is in the same position, for the opposite reason: the photographs of him are recent enough to be under copyright. They appear above as grey silhouettes with their initials. The photographs are therefore a fair sample of who is famous, not of who did this work, and the silhouettes are left visible rather than quietly omitted for that reason.