Foundations of mathematics

Formal proof with proof assistants (Lean)

A proof assistant like Lean checks a mathematical proof the way a compiler checks a program: it reduces "is this proof correct?" to "does this $\Gamma \vdash t : P$ typing judgment reduce", verified by a small trusted kernel.

IntuitionWhy trust a proof you cannot fully read?

Mathlib, the Lean 4 mathematical library, now has millions of lines of proof — far more than any one person can read line by line. Yet mathematicians trust it, for the same reason we trust an elevator inspector's stamp rather than personally re-welding every cable: a small, fixed checking procedure (the kernel) has verified every single step, and the kernel itself is short enough to audit by hand.

The dependency graph of a checked proof: each node is a lemma, each edge a use of an earlier result; the kernel walks every edge.

UndergraduateThe Calculus of Inductive Constructions

Definition: Terms, types, and the typing judgment

Lean's core logic is the Calculus of Inductive Constructions (CIC): a dependent type theory where types can depend on values (dependent function type $\Pi\,(x:A)\,B(x)$ , read "for every $x:A$ , a value of type $B(x)$ "), and new types are built by inductive declarations (natural numbers, lists, the propositional equality type). Every object is classified by the typing judgment $\Gamma \vdash t : P$ : "in context $\Gamma$ , the term $t$ has type $P$ ".

\Gamma \vdash t : P

Under the Curry–Howard correspondence, a proposition $P$ is itself a type, and a proof of $P$ is a term $t$ of that type — proving is programming. This is why type-checking, an algorithm that already had to exist to compile programs, is enough to check proofs.

\vdash t : P \;\Longrightarrow\; P

Two layers of a proof assistant
Layer	Job	Trust
Elaborator / tactics	Search for a proof term $t$ from high-level tactic scripts	Untrusted: bugs here only waste time
Kernel	Re-check that $t$ really has type $P$	Trusted: this is the de Bruijn criterion

AdvancedThe de Bruijn criterion and equality via Eq.rec

The de Bruijn criterion says a proof assistant is trustworthy when a small, independently-auditable kernel checks every proof term, so $|\text{kernel}| \ll |\text{tactic engine}|$ : soundness rests on a few hundred lines of code, not on the tactic engine that produced the term. Inductive equality $a = b$ is itself defined by one constructor $\mathrm{refl} : \forall\, a,\ a = a$ , and its eliminator $\mathsf{Eq.rec}$ (the J-rule) is the single primitive the kernel needs to derive every other property of equality.

\mathsf{Eq.rec} : \{C : \forall\, y,\ a=y \to \mathrm{Sort}\} \to C\,a\,(\mathrm{refl}\,a) \to \forall\, y\,(h:a=y),\, C\,y\,h

Theorem: Symmetry of equality from Eq.rec

There is a term $\mathrm{Eq.symm} : a = b \to b = a$ built only from $\mathrm{refl}_a : a = a$ and $\mathsf{Eq.rec}$ ; symmetry is a theorem of CIC, not an extra axiom.

Why is it true?

If equality needed a separate axiom for symmetry, transitivity, congruence, and so on, the trusted kernel would grow with every new fact about $=$ . Deriving them all from one eliminator keeps the kernel tiny.

Proof

Fix $a$ . We want a function taking $h : a = b$ (for arbitrary $b$ ) to a proof of $b = a$ . Apply $\mathsf{Eq.rec}$ with the motive $C(y, h) := (y = a)$ — a family of propositions indexed by the point $y$ and the proof $h$ connecting $a$ to $y$ .

The eliminator asks for a proof of the base case $C(a, \mathrm{refl}\,a)$ , i.e. of $a = a$ ; supply $\mathrm{refl}\,a$ itself. This is legal because the base case is always indexed by $\mathrm{refl}$ at the starting point $a$ .

$\mathsf{Eq.rec}$ then returns, for every $y$ and every $h : a = y$ , a proof of $C(y,h) = (y = a)$ . Instantiate $y := b,\ h := h$ : we obtain exactly a proof of $b = a$ .

Packaging this as $\mathrm{Eq.symm}\,h := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, y = a)\,(\mathrm{refl}\,a)\,b\,h$ gives the term of type $\mathrm{Eq.symm} : a = b \to b = a$ . The kernel accepts it purely by matching this application against the type signature of $\mathsf{Eq.rec}$ — no reasoning about "symmetry" as a concept is needed at the kernel level.

Theorem: Transitivity of equality from Eq.rec

There is a term $\mathrm{Eq.trans} : a = b \to b = c \to a = c$ built only from $\mathsf{Eq.rec}$ .

Why is it true?

Chaining equalities ( $a=b=c$ therefore $a=c$ ) is used in essentially every proof; if it were an axiom instead of a derived term, the kernel would have to trust that axiom rather than verify it by computation.

Proof

Fix $a,b$ and $h_1 : a = b$ . Given $h_2 : b = c$ for arbitrary $c$ , we want a proof of $a = c$ . Apply $\mathsf{Eq.rec}$ to $h_2$ with motive $C(y, h) := (a = y)$ , indexed by the point $y$ and the proof $h$ connecting $b$ to $y$ .

The base case required is $C(b, \mathrm{refl}\,b)$ , i.e. $a = b$ — exactly $h_1$ . So $h_1$ is the base-case proof supplied to $\mathsf{Eq.rec}$ .

$\mathsf{Eq.rec}$ then delivers, for every $c$ and every $h_2 : b = c$ , a proof of $C(c, h_2) = (a = c)$ , which is what we wanted.

So $\mathrm{Eq.trans}\,h_1\,h_2 := \mathsf{Eq.rec}\,(C := \lambda y\, h,\, a = y)\,h_1\,c\,h_2$ has type $\mathrm{Eq.trans} : a = b \to b = c \to a = c$ . Notice the pattern shared with symmetry: both proofs "transport" a fact along an equality by choosing the right motive $C$ , then let the kernel's fixed reduction rule for $\mathsf{Eq.rec}$ on $\mathrm{refl}$ do the actual work.

UndergraduateReal-world applications: from compilers to number theory

Formal proof is no longer a laboratory curiosity. CompCert, a C compiler formally verified in Coq, has a machine-checked proof that its generated assembly always behaves like the source program — a guarantee no test suite can give. AWS and Signal use formally verified cryptographic code (in tools like AWS's s2n TLS library, HACL and F) to remove entire classes of memory-safety and side-channel bugs. And in pure mathematics, Lean's Liquid Tensor Experiment (2020–2022) formalized a hard theorem of Peter Scholze in condensed mathematics, and Terence Tao's team formalized the Polynomial Freiman–Ruzsa (PFR) conjecture's proof in Lean within months of the human proof appearing in 2023.

Example: Type-checking a proof of $n+0=n$

Show, at the level of the kernel, why the term built by induction for $\forall\, n : \mathbb{N},\ n + 0 = n$ is accepted.

Solution

Addition on $\mathbb{N}$ is defined by recursion on the second argument: $n + 0 := n$ and $n + \mathrm{succ}\,m := \mathrm{succ}\,(n+m)$ . So the base case of the goal $n + 0 = n$ reduces by computation to $n = n$ , which is $\mathrm{refl}\,n$ — the kernel accepts it with no logical work at all, just unfolding a definition.

For a general theorem $\forall n,\ n + 0 = n$ this base case is trivial by the definition above, so no induction is even needed for this particular statement (unlike $\forall n,\ 0 + n = n$ , which does need induction since recursion is on the second argument).

The kernel's role is simply to unfold $+$ according to its recursive definition on the literal term $n+0$ , arrive at $n$ , and then check that the two sides of the goal are definitionally equal — reducing "is this proof correct" to a terminating computation, exactly the de Bruijn criterion in action.

Example: Verified compilation as a typed equality

CompCert states its correctness theorem as a semantic preservation property. Explain what "the proof is a term of that type" buys engineers over ordinary compiler testing.

Solution

CompCert's theorem has the shape "for every source program $S$ that compiles to assembly $A$ , every observable behavior of $A$ is a behavior of $S$ " — a universally quantified statement over all source programs, not just the ones in a test suite.

A test suite checks finitely many $(S,A)$ pairs and can never rule out a miscompilation on program #4,000,001. A Coq proof term $t$ of the universally quantified statement is instead type-checked once, for the whole quantifier, by the kernel — the same kernel used for every other CompCert lemma, so no new trust is introduced per test case.

Because the proof term is total and the theorem is about the compiler's actual Coq source code (extracted to OCaml), any change to the compiler that breaks the guarantee simply fails to type-check, catching regressions that a finite regression-test suite would miss entirely — this is precisely why CompCert-generated code has had zero miscompilation bugs found by fuzzing campaigns that found hundreds in GCC and Clang.

Research frontier as of 2026

Formalization is now fast enough to track research in near real time: Terence Tao's formalization of the PFR conjecture (2023) took weeks, not years, and the Lean community formalized Fermat's Last Theorem's special cases and large parts of the Liquid Tensor Experiment within a couple of years of the original arguments. Active fronts include AI-assisted tactic search (AlphaProof, DeepSeek-Prover) that proposes proof terms for the kernel to check, "blueprint"-driven collaborative formalization of frontier results (the Fermat Last Theorem project, Grothendieck's original EGA/SGA style redone as a Lean project), and formal verification spreading into everyday infrastructure (Rust's borrow checker research, verified rollup circuits in blockchains). The open bottleneck is not the kernel — the de Bruijn criterion has not been broken — but the human and AI labor of elaboration: turning an informal argument into a term the kernel can check at all.

What does the typing judgment $\Gamma \vdash t : P$ assert?

The de Bruijn criterion is best summarized as:

In the proof of $\mathrm{Eq.symm} : a = b \to b = a$ , what proposition is supplied for the base case $C(a, \mathrm{refl}\,a)$ ?

Which real-world system relies on a machine-checked proof that generated assembly always behaves like the source program?

References

Leonardo de Moura, Sebastian Ullrich (2021). The Lean 4 Theorem Prover and Programming Language
Xavier Leroy (2009). Formal verification of a realistic compiler
Terence Tao, et al. (2023). A Proof of the Polynomial Freiman-Ruzsa Conjecture · arXiv:2311.05762