Why formalize?

Interactive theorem proving with Lean -- first lecture.

What formalizing means

Write the proof in a language precise enough for a machine to check every step.

Autoformalizing runs the other way -- informal mathematics in, formal text out.

2026

Feb -- sphere packing, dimension 8: a machine finishes it in five days.

4 Sep -- Fermat's Last Theorem, checked. 11 days, 13 M lines of Lean.

8 Sep -- Navier-Stokes with a force: a singularity in finite time.

6 Oct -- 719 manuscripts, 42 % with a Lean proof.

FLT: Anthropic, Claude, building on Mathlib, following a simplified Wiles. Buzzard confirmed it assumes nothing but the axioms.

Navier-Stokes: the forced equation. Not the Millennium problem. The prize is unclaimed. Say this plainly.

February first, and it is the cleanest case: the statement was settled mathematics, only the formalizing was left.

One day after that catalogue, three of its manuscripts were withdrawn over a sign error, and fourteen more were revised. None of the withdrawn ones had a Lean proof. Say it; do not put it on the slide.

Machines now produce mathematics faster than mathematicians can referee it, and the only check that keeps up is a formal one. Do not oversell it -- the next slide takes it back a step.

But be precise

A Lean proof certifies that a formal statement follows from the axioms.

Whether that statement is the theorem in the paper is a human question.

Reading a formal statement and judging what it says is most of what this course teaches.

Where people are going

New GitHub repositories per quarter for Lean, Coq/Rocq and Isabelle, 2018 to 2026

New GitHub repositories per quarter for the three large proof assistants, counted per million new repositories overall.

Papers checked in Lean

Share of arXiv mathematics papers with a Lean-checked result during 2026, per 100 submissions

Papers on the mathematics arXiv whose results are checked in Lean, per 100 submissions, by week of submission in 2026.

The denominator doubled too: about 1 000 submissions a week in January, about 2 400 in September.

The idea is old

Gottlob Frege

Bertrand Russell

1879 -- Frege makes proofs into objects you can calculate with.

1902 -- Russell's letter: the system is inconsistent.

1910-13 -- Principia Mathematica rebuilds. 1 + 1 = 2 arrives in volume two.

Hilbert's programme, 1920s

David Hilbert

Kurt Gödel

Fix the language, fix the rules. A proof becomes a finite string, and checking it is a question about symbols.

Hilbert wants two more things: a consistency proof by finitary means, and a procedure deciding every question.

1931 -- Gödel: the consistency proof cannot exist.

1936: Church and Turing

Alonzo Church

Alan Turing

1928 -- Hilbert and Ackermann: is there a procedure deciding whether a formula is provable? The Entscheidungsproblem.

1936 -- Church and Turing, independently: there is none.

First they had to say what a procedure is. Turing built his machine. Church built the \lambda-calculus.

The lambda calculus

A notation for functions, and nothing else.

\lambda x.\, x + 1 is the function adding one. The only rule is substitution: (\lambda x.\, x + 1)\, 3 becomes 3 + 1.

Numbers, pairs and recursion are not built in. They are written as \lambda-terms, and that is enough for everything Turing's machines compute.

Lean is this notation with types on top:

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

Checking is not finding

Question	Answer
Does this text prove the statement?	decidable, and cheap
Find a proof of the statement.	semi-decidable: ends if one exists
Decide whether a proof exists.	undecidable (1936)

You prove. The machine checks. That split is a theorem, not a gap in today's software.

1967: the first checker

Nicolaas Govert de Bruijn

Automath -- a typed \lambda-calculus with dependent types, not set theory. The first machine-checked proofs.

1977 -- Landau's Grundlagen der Analysis through it, end to end.

Then Mizar 1973, LCF 1975, HOL, Isabelle 1986, Coq 1989.

The idea is 150 years old. The tool is 20.

De Bruijn starts Automath at Eindhoven in 1967 and publishes in 1968. He arrives at the Curry-Howard correspondence himself, not knowing Howard's work, and is the first to use it in a running system. Van Benthem Jutting's 1977 thesis pushes Landau's book through it: the first mathematics book verified end to end.

Two architectures come out of the next twenty years. LCF, Milner 1972 and 1975: thm is an abstract data type and only the inference rules can produce one, so nothing above the kernel needs trusting; ML was invented to write it. Automath's line instead writes down a proof term, which a small separate checker reads afterwards -- the de Bruijn criterion. Lean is in that line. A Lean proof is a term, and the kernel rechecks it whatever tactic produced it.

Lean itself: de Moura, Microsoft Research, 2013. Lean 4 in 2021. Lean FRO, about twenty people. Buzzard arguing for it since 2018.

How it got here

1976 -- the four colour theorem.

1998 -- the Kepler conjecture.

2013 -- Voevodsky concedes.

2020 -- the Liquid Tensor Experiment.

1976: four colours

A map of thirty-four regions coloured with four colours

Georges Gonthier

Appel and Haken reduce the problem to a list of configurations, and an ordinary program checks it -- no proof assistant.

No human has ever read that part.

2005: Gonthier redoes all of it in Coq, case analysis included.

The Kepler conjecture

A pyramid of equal spheres, the face-centred cubic packing

Thomas Hales

Hales announces a proof of Kepler's conjecture of 1611. Twelve referees, four years.

Verdict: ninety-nine percent certain -- and no better was possible. The Annals published it with the caveat attached.

Hales started Flyspeck. Complete formal proof in HOL Light and Isabelle, 2014.

2013: the author concedes

Vladimir Voevodsky

1989 -- Voevodsky and Kapranov identify \infty-groupoids with homotopy types.

Oct 1998 -- Simpson argues that it cannot be true, but cannot say which step.

Autumn 2013 -- Voevodsky accepts it. Fifteen years unused, and unrefuted.

Mathematics runs on a complex system of mutual trust based on reputations.

Note the dates: the paper is from 1989, but the episode only ends in 2013, which is why it sits here and not before Kepler.

Fifteen years, and not an obscure corner: both authors were well known, and Voevodsky received the Fields Medal in between, in 2002. Everyone makes mistakes. What matters here is how long it took to resolve, and why: nobody could point at the faulty step, so it was unclear who had erred, and nobody challenged them.

The quoted line is Voevodsky's own, from his 2014 IAS lecture.

Second story, same lesson: a mistake in a lemma of his own from 1992 stayed in print until someone checking his lectures step by step found it in 1999. Several seminars had read the paper by then.

His conclusion: a hard technical argument by a trusted author is hardly ever checked in detail.

He then looked for a proof assistant, found none he could use, and built the foundations for one: univalent foundations, the IAS special year 2012-13, the HoTT book. In Coq, not Lean, and not the foundations Mathlib uses. We take the diagnosis, not the cure. He died in 2017.

2020: a Fields medallist is unsure

Peter Scholze

Johan Commelin

Scholze posts a challenge on Buzzard's blog: a theorem in condensed mathematics he is not certain of.

Liquid Tensor Experiment, led by Commelin. Finished July 2022.

The request came from a working mathematician, not from logicians. That is what had changed.

Perfectoid spaces, 2019

Kevin Buzzard

Johan Commelin

Patrick Massot

The problem: could an object as complicated as Scholze's perfectoid space be stated at all in a proof assistant?

They formalized a definition, not a theorem. Stating is a different problem from proving.

Sphere eversion, 2022

Patrick Massot

Floris van Doorn

Oliver Nash

The problem: Mathlib had no differential geometry, and Gromov's h-principle needs it.

So they built the API first and proved the theorem afterwards. That order is the ordinary shape of the work.

Freiman-Ruzsa, 2023

Timothy Gowers

Ben Green

Terence Tao

Freddie Manners

The problem: a formalization took one team years, so it always came long after the paper.

A blueprint cuts the work into pieces with stated interfaces. Strangers in parallel, three weeks, before refereeing.

Equational Theories, 2024-25

The problem: 22 028 942 implications between 4 694 laws on magmas. Not deep -- but beyond any human team.

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

Sphere packing, dim. 8 and 24

Maryna Viazovska

The problem: the mathematics was finished in 2016, and formalizing it still took a human project two years.

In Lean, on Mathlib. An autoformalizer closed dimension 8 in five days, February 2026.

Three systems

System	Logic	Library
Lean 4	dependent types	one: Mathlib
Rocq (Coq until 2025)	dependent types	many packages
Isabelle/HOL	simple type theory	the AFP

Only Isabelle has no dependent types. Its automation is the strongest of the three.

We use Lean because Mathlib exists.

Mathlib

One library, one repository, one version. Everything in this course imports it.

The library itself

The interactive import map -- the whole of Mathlib as a graph of its areas.

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.

Where to start

Natural Number Game -- in the browser, nothing to install. Start here.

Formalising Mathematics -- Bhavik Mehta, after Kevin Buzzard.

Mathematics in Lean -- Avigad and Massot. The closest thing to an official course.

What your machine needs

Every sheet begins with import Mathlib, so a two-line sheet needs as much memory as the hardest one.

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

Below the minimum? Talk to us -- there is a server with 128 GB.

Wednesday

Bring a laptop. With administrator rights.

Follow the installation instructions in the course notes beforehand.

Then run lake exe cache get before you come.