Proof assistants and formal verification (Lean, mathlib)

A proof in a thesis is checked by its author, its supervisor and its examiners, all of them human and all of them fallible. A formal proof is checked by a computer program, line by line, down to the axioms. For most of the twentieth century formal proofs were a theoretical ideal; in the last two decades they have become practical for serious mathematics, and in the last few years spectacularly so. This lesson explains what proof assistants are, how they work, what has been formalized, and how an honors student might use one, whether to verify a key lemma, to learn mathematics more deeply, or as the center of a project.

What a proof assistant does

A proof assistant is a program in which you state definitions and theorems in a precise formal language and construct proofs that the program checks. The checking is done by a small trusted component called the kernel, which accepts a proof only if every step follows from the rules of the underlying logic. Everything else in the system, including the automation that finds proof steps for you, produces proof terms that the kernel rechecks. So a bug in the automation can cause a proof attempt to fail but cannot cause a false theorem to be accepted; only a bug in the small kernel, or a wrong formal statement, could do that.

The last point deserves emphasis. A proof assistant verifies that the formal statement follows from the axioms. It cannot verify that the formal statement says what you meant. If you formalize the wrong definition, for instance by using natural-number subtraction, which truncates at zero, where you meant integer subtraction, the assistant will happily prove the wrong theorem. Checking that formal statements match their informal meaning remains a human responsibility, and in large projects it is done by careful review of the statements, which are far shorter than the proofs.

Several mature proof assistants exist. Isabelle/HOL and HOL Light are based on higher-order logic; the Coq system, renamed Rocq in 2025, and Lean are based on dependent type theory, in which propositions are types and proofs are terms of those types. Agda and Metamath are further examples. Lean, created by Leonardo de Moura at Microsoft Research from 2013 and now developed by the nonprofit Lean Focused Research Organization, has become the most widely used by research mathematicians, largely because of its community library.

Mathlib

Mathlib is a single, unified library of formalized mathematics for Lean, built and maintained by a community of hundreds of contributors since 2017. It covers algebra, analysis, topology, measure theory, number theory, combinatorics, category theory, geometry and more, at roughly the level of an undergraduate degree plus substantial parts of graduate mathematics. In late 2026 its statistics page listed about 140,000 definitions and 290,000 theorems by more than 770 contributors. The library migrated from Lean 3 to Lean 4 in a project completed in 2023. Its design principle is unity: there is one definition of a group, one of a measure, one of the real numbers, and everything is built to work together, which is what makes large formalizations possible.

New contributions to mathlib are reviewed by maintainers for correctness, generality and style, much as papers are refereed. A student project that formalizes a modest piece of mathematics, such as Amara's Theorem 2, can sometimes be contributed to mathlib, which is a genuine and lasting contribution to mathematics.

Landmarks of formalization

The four-color theorem was formalized in Coq by Georges Gonthier and Benjamin Werner in 2005, and the Feit–Thompson odd order theorem, whose original proof runs to 255 pages, by Gonthier's team in 2012. The Flyspeck project completed a formal proof of the Kepler conjecture in HOL Light and Isabelle in 2014.

In December 2020 Peter Scholze challenged the community to formalize a central theorem of the condensed mathematics he had developed with Dustin Clausen, a result whose proof he was not entirely sure of himself. The Liquid Tensor Experiment, led by Johan Commelin, formalized the key technical statement in Lean within six months and completed the full challenge in July 2022. Scholze reported that the process had improved his understanding of the proof. In November 2023 Timothy Gowers, Ben Green, Freddie Manners and Terence Tao proved the polynomial Freiman–Ruzsa conjecture in additive combinatorics; a collaborative project coordinated by Tao formalized the proof in Lean in about three weeks.

Kevin Buzzard of Imperial College London began a project in 2024 to formalize the proof of Fermat's Last Theorem, planned as a multi-year effort that would reduce the theorem to results proved in the 1980s and then continue. In September 2026 Anthropic reported that its Claude model, working largely autonomously over about eleven days and building on pieces of Buzzard's project and on mathlib, had produced a complete Lean proof of Fermat's Last Theorem following a simplified form of the Wiles argument; Buzzard, after reviewing it, said that it proves the theorem with no assumptions beyond the axioms of mathematics. Whatever its long-term significance, the episode illustrates both the maturity of the tools and why formal verification matters when proofs are produced by machines: the kernel's check does not depend on trusting the author, human or not.

A first look at Lean

Here is the flavor of Lean 4 with mathlib. A theorem has a name, hypotheses, a statement after the colon, and a proof after the symbol :=. The proof may be a term or, more commonly, a sequence of tactics after the keyword by. Each tactic transforms the current goal; the proof is complete when no goals remain. The first example defines the sum of the first \(n\) odd numbers recursively and proves it equals \(n^2\) by induction.

import Mathlib.Tactic

def sumOdd : Nat → Nat
  | 0 => 0
  | n + 1 => sumOdd n + (2 * n + 1)

theorem sumOdd_eq (n : Nat) : sumOdd n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [sumOdd, ih]
    ring

Read it as an informal proof. The induction tactic splits the goal into a base case and an inductive step. In the base case, sumOdd 0 is 0 by definition and \(0 \cdot 0\) computes to 0, so rfl, reflexivity of equality after computation, closes it. In the inductive step the goal is sumOdd (k + 1) = (k + 1) * (k + 1), with the hypothesis ih : sumOdd k = k * k. The simp only tactic unfolds the definition and rewrites with ih, leaving k * k + (2 * k + 1) = (k + 1) * (k + 1), an identity of commutative semirings that the ring tactic proves by normalizing both sides.

The second example uses mathlib's big-operator notation for sums over a finite range and proves Gauss's formula in a doubled form that avoids division, a standard trick in formalization since division on natural numbers rounds down.

import Mathlib

open Finset

theorem gauss_sum (n : ℕ) : 2 * ∑ i ∈ range (n + 1), i = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ k ih =>
    rw [sum_range_succ, mul_add, ih]
    ring

-- mathlib already knows that there are infinitely many primes
theorem primes_unbounded (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime :=
  Nat.exists_infinite_primes n

The rewrite tactic rw uses equations from the library: sum_range_succ splits off the last term of the sum, mul_add distributes the factor 2, and ih replaces the doubled sum up to \(k\) by \(k(k + 1)\). The remaining goal \(k(k + 1) + 2(k + 1) = (k + 1)(k + 2)\) is closed by ring. The second theorem is a one-line application of a mathlib result; finding the names of such results, using the library's search tools and documentation, is a large part of practical formalization.

Finally, Lean is also a programming language, and definitions can be evaluated. A computable version of Amara's representation count can be checked on small cases by evaluation inside the proof assistant, so that statements about specific numbers are proved by computation in the kernel.

-- number of k with k(k+1) <= 2n and 2k dividing 2n - k(k-1): the representation count
def reps (n : Nat) : Nat :=
  ((List.range (n + 1)).filter fun k =>
    decide (1 ≤ k) && decide (k * (k + 1) ≤ 2 * n) && (2 * n - k * (k - 1)) % (2 * k) == 0).length

#eval (List.range 16).map reps    -- [0, 1, 1, 2, 1, 2, 2, 2, 1, 3, 2, 2, 2, 2, 2, 4]

example : reps 15 = 4 := by decide
example : reps 64 = 1 := by decide

How proof checking works: a tiny kernel

The idea of a trusted kernel can be illustrated with a few lines of Python. The program below checks proofs in a minimal propositional logic with only implication, two axiom schemes and the rule of modus ponens, which from \(A\) and \(A \to B\) infers \(B\). The axiom schemes are \(K: A \to (B \to A)\) and \(S: (A \to (B \to C)) \to ((A \to B) \to (A \to C))\). A proof is a list of formulas, each of which must be an instance of an axiom scheme or follow by modus ponens from two earlier lines. The checker does not search for proofs; it only verifies them, and it is short enough to trust by inspection. That separation between finding and checking is exactly the architecture of Lean.

def imp(a, b):
    return ('->', a, b)

def is_K(f):          # A -> (B -> A)
    return f[0] == '->' and f[2][0] == '->' and f[2][2] == f[1]

def is_S(f):          # (A -> (B -> C)) -> ((A -> B) -> (A -> C))
    try:
        (_, (_, a, (_, b, c)), (_, (_, a2, b2), (_, a3, c2))) = f
        return a == a2 == a3 and b == b2 and c == c2
    except (TypeError, ValueError):
        return False

def check(proof, goal):
    for i, f in enumerate(proof):
        by_axiom = isinstance(f, tuple) and (is_K(f) or is_S(f))
        by_mp = any(g == imp(h, f) for g in proof[:i] for h in proof[:i])
        if not (by_axiom or by_mp):
            return f"line {i + 1} is not justified"
    return "proof accepted" if proof and proof[-1] == goal else "last line is not the goal"

A = 'A'
AA = imp(A, A)
proof = [
    imp(imp(A, imp(AA, A)), imp(imp(A, AA), AA)),   # S with B = A -> A, C = A
    imp(A, imp(AA, A)),                              # K
    imp(imp(A, AA), AA),                             # modus ponens, lines 2 and 1
    imp(A, AA),                                      # K
    AA,                                              # modus ponens, lines 4 and 3
]
print("A -> A:", check(proof, AA))
print("with line 2 removed:", check(proof[:1] + proof[2:], AA))
print("claiming A from nothing:", check([A], A))

A -> A: proof accepted
with line 2 removed: line 2 is not justified
claiming A from nothing: line 1 is not justified

The five-line proof of \(A \to A\) is the classic demonstration that even trivial-looking statements need proof in a formal system. Real proof assistants work in vastly richer logics and provide powerful automation, but the principle is the same: whatever produced the proof, a small checker decides whether to accept it.

Blueprints and large formalizations

Large formalization projects are organized around a blueprint, a human-readable document, written in LaTeX with tools developed by Patrick Massot, that breaks the proof into definitions and lemmas, records which depend on which, and tracks which have been stated and proved formally. Contributors pick a lemma whose dependencies are done, formalize it and mark it complete. The dependency graph shows progress at a glance. The same structure is useful for planning the proofs in a thesis, formal or not: it makes explicit which results depend on which, and therefore where a gap would be most damaging.

# a blueprint for the model thesis: node -> (dependencies, formalized?)
blueprint = {
    'def: representation':       ([], True),
    'lemma: sum formula':        (['def: representation'], True),
    'lemma: opposite parity':    (['lemma: sum formula'], True),
    'thm 1: non-powers of two':  (['lemma: opposite parity'], False),
    'thm 2: odd divisors':       (['lemma: opposite parity'], False),
    'cor 3: odd lengths':        (['thm 2: odd divisors'], False),
    'cor 4: length spectrum':    (['thm 2: odd divisors'], False),
    'thm 5: all integers':       (['thm 2: odd divisors'], False),
}

def depth(node, memo={}):
    if node not in memo:
        deps = blueprint[node][0]
        memo[node] = 1 + max((depth(d) for d in deps), default=0)
    return memo[node]

done = {n for n, (d, f) in blueprint.items() if f}
ready = [n for n, (d, f) in blueprint.items() if not f and all(x in done for x in d)]
blocked = [n for n, (d, f) in blueprint.items() if not f and n not in ready]
print(f"formalized {len(done)} of {len(blueprint)}")
print("ready to formalize now:", ready)
print("blocked:", blocked)
print("longest dependency chain:", max(depth(n) for n in blueprint))

formalized 3 of 8
ready to formalize now: ['thm 1: non-powers of two', 'thm 2: odd divisors']
blocked: ['cor 3: odd lengths', 'cor 4: length spectrum', 'thm 5: all integers']
longest dependency chain: 5

Formalization in an honors project

There are several ways a proof assistant can enter an honors project. A student can formalize one key lemma or theorem of an otherwise conventional thesis, as an appendix that adds certainty and demonstrates a technical skill. A student can make formalization the project itself, choosing a result not yet in mathlib, such as a classical theorem from number theory or combinatorics, and contributing it to the library. Or a student can study formalization as a subject: comparing proof assistants, analyzing how informal proofs must be restructured to be formalized, or experimenting with automation and AI systems for proof search.

Formalization is slower than writing informal proofs, often by a factor of ten or more for a newcomer, and the learning curve is steep. The rewards are a level of understanding that informal writing rarely forces, since every implicit step must be made explicit, and a result that is checked beyond reasonable doubt. Students considering a formalization project should work through an introductory resource such as the Natural Number Game, an online tutorial that develops arithmetic from Peano's axioms, and the book Mathematics in Lean, and should talk to a supervisor with experience, since the community's conventions matter a great deal.