Formalising mathematics in Lean and Mathlib

In 1998 Thomas Hales announced a proof of the Kepler conjecture: no packing of equal spheres in space is denser than the familiar pyramid of oranges on a market stall. The proof combined hundreds of pages of argument with extensive computer calculations, and after years of work the referees said they were "99% certain" it was correct. Hales responded by leading the Flyspeck project, which by 2014 had checked the entire proof in the proof assistants HOL Light and Isabelle. In 2020 Peter Scholze challenged the community to check a difficult theorem of his and Dustin Clausen's in condensed mathematics; the Liquid Tensor Experiment, carried out in Lean by a team coordinated by Johan Commelin, completed the task in 2022, and Scholze reported that the work had improved his own understanding of the proof.

A proof assistant is a program in which definitions, theorem statements and proofs are written in a precise formal language, and a small trusted core — the kernel — checks that every step follows from the rules. Mathematicians formalise to gain certainty about long or computer-assisted proofs, to build a searchable library of mathematics, and — increasingly — simply because it is a superb way to learn exactly what a proof needs.

This lesson continues first steps in Lean, where you met rfl, rw, simp and induction. Here we formalise the everyday material of a first university course — sets and functions, quantifiers, limits, algebraic structures — in Lean 4 with Mathlib, the community's mathematical library.

In Lean every expression has a type. 3 : ℕ says that $3$ is a natural number; fun n => n + 1 : ℕ → ℕ is a function. A mathematical statement is also a type, of the special sort Prop, and a proof of the statement is an object of that type. To prove $P \to Q$ is to construct a function that turns any proof of $P$ into a proof of $Q$; to prove $\forall x, P(x)$ is to construct a function sending each $x$ to a proof of $P(x)$; to prove $\exists x, P(x)$ is to supply a witness together with a proof about it. This correspondence between propositions and types is the Curry–Howard correspondence.

Writing proof objects by hand is tedious, so we usually write tactics: instructions such as intro, apply, rw, obtain and exact that transform the current goal (what remains to be shown, with the hypotheses available) step by step, while Lean builds the proof object behind the scenes. Here is the proof that a composite of injections is injective; read it alongside the comments.

/-- **A composite of injections is injective**, proved as on paper: if `g (f x) = g (f y)`,
then `f x = f y` because `g` is injective, and then `x = y` because `f` is injective. -/
theorem injective_comp {α β γ : Type*} {f : α → β} {g : β → γ} (hg : Injective g)
    (hf : Injective f) : Injective (g ∘ f) := by
  intro x y h
  -- `h : (g ∘ f) x = (g ∘ f) y`, which is `g (f x) = g (f y)` by definition.
  apply hf
  apply hg
  exact h

After intro x y h the goal is x = y, with h : (g ∘ f) x = (g ∘ f) y. apply hf says: "it suffices to show f x = f y, since f is injective"; apply hg reduces that to g (f x) = g (f y); and exact h finishes, because (g ∘ f) x is by definition g (f x). The kernel then checks the finished proof object — however it was produced.

In Lean, part (b) eliminates two existential statements with obtain, and the pattern rfl substitutes the equation it obtains; part (c) is the human proof almost word for word. Mathlib has part (a) already — the theorem is found by exact?, or by guessing its name from Mathlib's conventions (the conclusion Injective (g ∘ f) becomes Injective.comp):

/-- **A composite of surjections is surjective.** Given `z`, choose `y` with `g y = z`, then
`x` with `f x = y`; then `g (f x) = z`. Each "choose" is the elimination of an `∃`. -/
theorem surjective_comp {α β γ : Type*} {f : α → β} {g : β → γ} (hg : Surjective g)
    (hf : Surjective f) : Surjective (g ∘ f) := by
  intro z
  obtain ⟨y, rfl⟩ := hg z
  obtain ⟨x, rfl⟩ := hf y
  exact ⟨x, rfl⟩

/-- If `g ∘ f` is injective then `f` is injective (but `g` need not be). -/
theorem injective_of_comp {α β γ : Type*} {f : α → β} {g : β → γ} (h : Injective (g ∘ f)) :
    Injective f := by
  intro x y hxy
  apply h
  show g (f x) = g (f y)
  rw [hxy]

/-- The same theorem, found in Mathlib: `Function.Injective.comp`. Its name follows Mathlib's
naming convention — the conclusion's shape, `Injective (g ∘ f)`, read as `Injective.comp` — and
it can be found by `exact?` or by searching the documentation. -/
theorem injective_comp_library {α β γ : Type*} {f : α → β} {g : β → γ} (hg : Injective g)
    (hf : Injective f) : Injective (g ∘ f) :=
  hg.comp hf

Sets. In Mathlib a set of elements of type α is a predicate: Set α is α → Prop, and x ∈ s means s x. The image f '' s is the set of y for which ∃ x, x ∈ s ∧ f x = y, and the preimage f ⁻¹' t is the set of x with f x ∈ t. Two sets are equal when they have the same elements (extensionality, the tactic ext).

/-- `f(s ∪ t) = f(s) ∪ f(t)`, by extensionality: show that an arbitrary `y` lies in the left
side exactly when it lies in the right side. (Mathlib: `Set.image_union`.) -/
theorem image_union {α β : Type*} (f : α → β) (s t : Set α) :
    f '' (s ∪ t) = f '' s ∪ f '' t := by
  ext y
  constructor
  · rintro ⟨x, hx | hx, rfl⟩
    · exact Or.inl ⟨x, hx, rfl⟩
    · exact Or.inr ⟨x, hx, rfl⟩
  · rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩)
    · exact ⟨x, Or.inl hx, rfl⟩
    · exact ⟨x, Or.inr hx, rfl⟩

/-- `f(s ∩ t) ⊆ f(s) ∩ f(t)` always holds. -/
theorem image_inter_subset {α β : Type*} (f : α → β) (s t : Set α) :
    f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
  rintro y ⟨x, ⟨hs, ht⟩, rfl⟩
  exact ⟨⟨x, hs, rfl⟩, ⟨x, ht, rfl⟩⟩

/-- …but equality can fail. With the constant function `f = 0` on `ℕ`, `s = {0}` and `t = {1}`:
`f(s ∩ t) = f(∅) = ∅`, while `f(s) ∩ f(t) = {0}`. -/
theorem image_inter_ne :
    ∃ (f : ℕ → ℕ) (s t : Set ℕ), f '' (s ∩ t) ≠ f '' s ∩ f '' t := by
  refine ⟨fun _ => 0, {0}, {1}, ?_⟩
  intro h
  have h0 : (0 : ℕ) ∈ (fun _ : ℕ => (0 : ℕ)) '' {0} ∩ (fun _ : ℕ => (0 : ℕ)) '' {1} :=
    ⟨⟨0, rfl, rfl⟩, ⟨1, rfl, rfl⟩⟩
  rw [← h] at h0
  obtain ⟨x, ⟨hx0, hx1⟩, -⟩ := h0
  rw [mem_singleton_iff] at hx0 hx1
  omega

/-- For an *injective* `f`, equality does hold: Mathlib's `Set.image_inter`. The hypothesis
`Injective f` is exactly what the counterexample above lacks. -/
theorem image_inter_of_injective {α β : Type*} {f : α → β} (hf : Injective f) (s t : Set α) :
    f '' (s ∩ t) = f '' s ∩ f '' t :=
  Set.image_inter hf

/-- Preimages behave perfectly: `f⁻¹(s ∩ t) = f⁻¹(s) ∩ f⁻¹(t)`. In Lean both sides unfold to the
same predicate `fun x => f x ∈ s ∧ f x ∈ t`, so the proof is `rfl`: true *by definition*. -/
theorem preimage_inter {α β : Type*} (f : α → β) (s t : Set β) :
    f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t :=
  rfl

The rintro patterns in the first proof do a lot at once: ⟨x, hx | hx, rfl⟩ introduces a witness x, splits the "or" into two cases, and substitutes y = f x. Part (c) is true by definition — after unfolding, both sides are the same predicate — so its proof is rfl. That preimages behave better than images is a familiar fact in topology, and here the formal system shows exactly why.

Every quantifier step has a tactic:

The order of quantifiers matters, and formalisation never lets you forget it.

/-- `∃ x, ∀ y, P x y` implies `∀ y, ∃ x, P x y`: a single `x` that works for every `y` certainly
gives, for each `y`, some `x`. -/
theorem exists_forall_imp {α β : Type*} (P : α → β → Prop) :
    (∃ x, ∀ y, P x y) → ∀ y, ∃ x, P x y := by
  rintro ⟨x, hx⟩ y
  exact ⟨x, hx y⟩

/-- The converse fails: every natural number has a larger one (`∀ n, ∃ m, n < m`), but no
natural number is larger than all of them (`∃ m, ∀ n, n < m` is false — take `n = m`). -/
theorem forall_exists_not_imp :
    ¬ ((∀ n : ℕ, ∃ m, n < m) → ∃ m : ℕ, ∀ n, n < m) := by
  intro h
  obtain ⟨m, hm⟩ := h (fun n => ⟨n + 1, Nat.lt_succ_self n⟩)
  exact lt_irrefl m (hm m)

Limits. The definition of convergence is a $\forall\exists\forall$ statement. Written in Lean exactly as in an analysis course, it can be used to prove the standard first results — and the proofs have the same shape as on paper.

/-- The ε–N definition of convergence of a real sequence, written exactly as in an analysis
course: for every `ε > 0` there is `N` such that `|aₙ − L| < ε` for all `n ≥ N`. -/
def ConvergesTo (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

/-- `1/(n + 1) → 0`. Given `ε > 0`, the Archimedean property gives `N > 1/ε`; then for `n ≥ N`,
`1/(n + 1) < 1/N < ε`. -/
theorem converges_one_div : ConvergesTo (fun n => 1 / ((n : ℝ) + 1)) 0 := by
  intro ε hε
  obtain ⟨N, hN⟩ := exists_nat_gt (1 / ε)
  refine ⟨N, fun n hn => ?_⟩
  have hn' : (N : ℝ) ≤ n := by exact_mod_cast hn
  have hpos : (0 : ℝ) < (n : ℝ) + 1 := by positivity
  rw [sub_zero, abs_of_pos (by positivity)]
  rw [div_lt_iff₀ hpos]
  rw [div_lt_iff₀ hε] at hN
  nlinarith

/-- **Limits are unique.** If `a → L` and `a → M` with `L ≠ M`, take `ε = |L − M|/2`: for large
`n`, `|L − M| ≤ |aₙ − L| + |aₙ − M| < 2ε = |L − M|`, a contradiction. -/
theorem limit_unique {a : ℕ → ℝ} {L M : ℝ} (hL : ConvergesTo a L) (hM : ConvergesTo a M) :
    L = M := by
  by_contra hne
  have hε : 0 < |L - M| / 2 := by
    have : 0 < |L - M| := abs_pos.mpr (sub_ne_zero.mpr hne)
    linarith
  obtain ⟨N₁, h₁⟩ := hL _ hε
  obtain ⟨N₂, h₂⟩ := hM _ hε
  have k₁ := h₁ (max N₁ N₂) (le_max_left _ _)
  have k₂ := h₂ (max N₁ N₂) (le_max_right _ _)
  have tri : |L - M| ≤ |a (max N₁ N₂) - L| + |a (max N₁ N₂) - M| := by
    calc |L - M| = |(a (max N₁ N₂) - M) - (a (max N₁ N₂) - L)| := by ring_nf
      _ ≤ |a (max N₁ N₂) - M| + |a (max N₁ N₂) - L| := abs_sub _ _
      _ = |a (max N₁ N₂) - L| + |a (max N₁ N₂) - M| := add_comm _ _
  linarith

But is ConvergesTo the right definition? Lean cannot answer that: it will happily check proofs about a definition that does not mean what you intended. Mathlib defines convergence differently — with filters, Tendsto a atTop (𝓝 L), a single notion that covers limits of sequences, of functions at a point, at infinity, from one side, and in any topological space. The following theorem checks that the two definitions agree, so every Mathlib theorem about Tendsto applies to our definition:

/-- **Does our definition mean what Mathlib means?** Mathlib defines convergence with filters:
`Tendsto a atTop (𝓝 L)`. Mathlib's `Metric.tendsto_atTop` unfolds it to the ε–N form with
`dist (a n) L`, and `Real.dist_eq` says `dist x y = |x − y|`. So the two definitions agree, and
every Mathlib theorem about `Tendsto` applies to `ConvergesTo`. -/
theorem convergesTo_iff_tendsto (a : ℕ → ℝ) (L : ℝ) :
    ConvergesTo a L ↔ Tendsto a atTop (𝓝 L) := by
  rw [Metric.tendsto_atTop]
  simp only [ConvergesTo, Real.dist_eq]

This is the most important habit of formalisation: a formal library is useful only if its definitions match standard mathematical usage, and that match is checked by people — by reading definitions, testing them on examples, and proving equivalences like this one.

A monoid is a set with an associative operation and a two-sided unit. In Lean that description becomes a class whose fields are the operations and the laws; an instance provides them for a particular type, and a theorem proved for an arbitrary instance holds for all of them.

/-- A home-made **type class** for monoids: a type `M` with a multiplication and a unit, and the
three laws as fields. A *structure* bundles data and proofs; declaring it as a `class` lets Lean
find an instance automatically. (Mathlib's real `Monoid` is built the same way, from smaller
classes such as `Mul`, `One` and `Semigroup`.) -/
class MyMonoid (M : Type*) where
  mul : M → M → M
  one : M
  mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a, mul one a = a
  mul_one : ∀ a, mul a one = a

/-- An **instance**: the natural numbers under addition form a monoid with unit `0`. The laws
are discharged by core lemmas about `Nat`. -/
instance natAddMyMonoid : MyMonoid ℕ where
  mul := (· + ·)
  one := 0
  mul_assoc := Nat.add_assoc
  one_mul := Nat.zero_add
  mul_one := Nat.add_zero

/-- **The unit of a monoid is unique**, proved once for *every* instance of `MyMonoid`: if `e`
is a two-sided unit then `e = one`, because `e = e · one = one`. -/
theorem MyMonoid.one_unique {M : Type*} [MyMonoid M] (e : M)
    (he : ∀ a : M, MyMonoid.mul e a = a ∧ MyMonoid.mul a e = a) :
    e = MyMonoid.one :=
  calc e = MyMonoid.mul e MyMonoid.one := (MyMonoid.mul_one e).symm
    _ = MyMonoid.one := (he MyMonoid.one).1

/-- Using the generic theorem at the instance for `ℕ`: a number `e` with `e + a = a` and
`a + e = a` for all `a` must be `0`. Lean finds `natAddMyMonoid` by instance search. -/
theorem zero_unique_nat (e : ℕ) (he : ∀ a : ℕ, e + a = a ∧ a + e = a) : e = 0 :=
  MyMonoid.one_unique e he

/-- In any Mathlib `Monoid`, a left inverse and a right inverse of the same element agree:
`b = b (a c) = (b a) c = c`. -/
theorem inv_unique {M : Type*} [Monoid M] {a b c : M} (hb : b * a = 1) (hc : a * c = 1) :
    b = c :=
  calc b = b * (a * c) := by rw [hc, mul_one]
    _ = b * a * c := (mul_assoc b a c).symm
    _ = c := by rw [hb, one_mul]

In the last proof Monoid is Mathlib's class. Mathlib organises algebra as a hierarchy of classes — Semigroup, Monoid, Group, CommGroup, Ring, CommRing, Field, ordered and normed variants, modules and algebras — linked so that every group is automatically a monoid, every field a ring, and so on. A lemma proved at the most general level (here, any monoid) is available everywhere below it.

/-- **A group in which every element squares to `1` is commutative.** From `x x = 1` we get
`x⁻¹ = x` for every `x`, so `a b = (a b)⁻¹ = b⁻¹ a⁻¹ = b a`. This works in *every* `Group`,
because the proof uses only the group laws (Mathlib lemmas `inv_eq_of_mul_eq_one_right` and
`mul_inv_rev`). -/
theorem comm_of_sq_eq_one {G : Type*} [Group G] (h : ∀ x : G, x * x = 1) (a b : G) :
    a * b = b * a := by
  have hinv : ∀ x : G, x⁻¹ = x := fun x => inv_eq_of_mul_eq_one_right (h x)
  calc a * b = (a * b)⁻¹ := (hinv (a * b)).symm
    _ = b⁻¹ * a⁻¹ := mul_inv_rev a b
    _ = b * a := by rw [hinv a, hinv b]

For identities in commutative rings, the ring tactic does all the work by normalising both sides as polynomials; the theorem then holds in $\Z$, $\Q$, $\R$, $\Z/n\Z$ and every other commutative ring Mathlib knows:

/-- In every commutative ring, `(a + b)² = a² + 2ab + b²`. The `ring` tactic decides such
identities by normalising both sides; the theorem then holds in `ℤ`, `ℚ`, `ℝ`, `ℤ/nℤ`,
polynomial rings, … at once. -/
theorem add_sq_comm_ring {R : Type*} [CommRing R] (a b : R) :
    (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

A formal system must say what every expression means, including expressions mathematicians avoid. In Lean and Mathlib, x / 0 = 0 and, for natural numbers, 2 - 3 = 0. These are conventions that make division and subtraction total functions; they do not change mathematics, because the theorems that would be false without a hypothesis carry that hypothesis.

/-- In Lean and Mathlib, `x / 0 = 0` (`div_zero`). This is a convention making division a total
function; it does not change any theorem about division by non-zero numbers. -/
theorem div_zero_convention (x : ℝ) : x / 0 = 0 :=
  div_zero x

/-- The familiar cancellation law carries its hypothesis explicitly: if `b ≠ 0` then
`a / b · b = a` (`div_mul_cancel₀`). -/
theorem div_mul_cancel_of_ne (a : ℝ) {b : ℝ} (hb : b ≠ 0) : a / b * b = a :=
  div_mul_cancel₀ a hb

/-- Without the hypothesis the law is false: `1 / 0 · 0 = 0 ≠ 1`. So the convention `x / 0 = 0`
cannot be used to "prove" anything false about real division. -/
theorem div_mul_cancel_needs_hyp : ¬ ∀ a b : ℝ, a / b * b = a := by
  intro h
  have := h 1 0
  norm_num at this

/-- Subtraction on `ℕ` is **truncated**: `2 − 3 = 0`, because there is no natural number
`−1`. -/
theorem nat_sub_truncates : (2 : ℕ) - 3 = 0 := by
  decide

/-- So `(a − b) + b = a` needs the hypothesis `b ≤ a` (`Nat.sub_add_cancel`); for `a = 2`,
`b = 3` the left side is `3`. -/
theorem nat_sub_add_cancel {a b : ℕ} (h : b ≤ a) : a - b + b = a :=
  Nat.sub_add_cancel h

So nothing false follows from $1/0 = 0$: to "cancel" $b$ in $a/b \cdot b = a$ you must supply a proof of $b \ne 0$. What the convention changes is where the hypothesis appears — on the cancellation law rather than on every use of division — which makes many statements shorter and some proofs easier.

Formalisation exposes hidden assumptions of other kinds too. A paper proof may silently use that a set is non-empty, that a function is defined everywhere, that two copies of "the same" structure really are the same, or that a case is "similar". Lean asks for each one. Experience from projects such as the Liquid Tensor Experiment is that formalisation is rarely mere translation: it often clarifies statements, finds small gaps and occasionally real errors, and sometimes suggests better proofs.

Searching and reusing. Before proving anything, look for it. Mathlib names follow conventions (mul_comm, add_le_add, Function.Injective.comp, Set.image_union); exact? searches the library for a lemma that closes the goal, apply? for lemmas whose conclusion fits, and simp? and rw? suggest rewrites; #check shows a statement. The documentation website and the Loogle search engine search by name and by the shape of a statement, and the Lean Zulip chat is where questions are answered. Citing a library lemma gives a short proof that inherits years of review and is maintained as the library changes; proving from scratch teaches you the argument and is necessary when the result is missing. This lesson's Lean file does both and labels each declaration accordingly.

Everything displayed in this lesson was compiled by Lean, and the website shows exactly the code that compiled. What does that guarantee?

• Every step follows from the rules of Lean's type theory and the axioms the proof uses. #print axioms makes the axioms visible. For this lesson's file it reports, for instance, that injective_comp, surjective_comp and nat_sub_truncates depend on no axioms at all; comm_of_sq_eq_one uses only propext; image_inter_ne uses propext and Quot.sound; and limit_unique, which argues by contradiction on real numbers, uses all three standard axioms, including Classical.choice. A proof with a gap would show sorryAx; the Lumenary's build refuses any.
• Not that the statement means what you think. If a definition is wrong, or a hypothesis is accidentally contradictory, Lean checks a correct proof of the wrong statement. That is why we proved convergesTo_iff_tendsto, why exercises below ask which formal statement matches an informal one, and why the Lumenary labels every declaration as independent, library or definition rather than claiming more.
• Trust in the checker. Lean's kernel is small, and independent re-implementations of kernel checkers exist for Lean 4 proofs; still, one trusts the kernel, the compiler that built it, and the hardware. This residual trust is far smaller than the trust needed in a long proof checked only by eye.

The Lean exercises for this lesson (in formal/LumenaryExercises/FormalProofLean.lean) ask you to reprove surjective_comp, exists_forall_imp and inv_unique from their statements; the solutions are the declarations above.

Before trying to prove a statement it is wise to test it on small cases. The first experiment checks the claims of Theorems 1–3 on every function and relation between sets with at most three elements. An exhaustive search over a finite universe can refute a general claim — one counterexample suffices — but never prove it for all sets.

"""Checking statements about sets and functions on every small example.

Before proving a statement in Lean it pays to test it. Here we check, on all
functions between sets of size at most 3:

* f(S & T) = f(S) & f(T) for all subsets S, T holds exactly when f is
  injective (Mathlib's Set.image_inter needs that hypothesis);
* if g o f is injective then f is injective - and g need not be;
* for every relation P on small sets, "exists x, for all y, P(x, y)" implies
  "for all y, exists x, P(x, y)", but not conversely.

An exhaustive search over a finite universe can refute a general claim (one
counterexample suffices) but can never prove it for all sets.
"""

import itertools

def functions(a, b):
    """All functions from range(a) to range(b), as tuples of values."""
    return list(itertools.product(range(b), repeat=a))

def subsets(n):
    """All subsets of range(n), as frozensets."""
    return [frozenset(c) for k in range(n + 1)
            for c in itertools.combinations(range(n), k)]

def image(f, s):
    """The image f(s) of a set s under a function given as a tuple."""
    return frozenset(f[x] for x in s)

def is_injective(f):
    """True if no two inputs share an output."""
    return len(set(f)) == len(f)

def preserves_intersections(f):
    """True if f(S & T) == f(S) & f(T) for all subsets S, T of the domain."""
    subs = subsets(len(f))
    return all(image(f, s & t) == image(f, s) & image(f, t)
               for s in subs for t in subs)

def compose(g, f):
    """The composite g o f of functions given as tuples."""
    return tuple(g[y] for y in f)

def exists_forall(rel, a, b):
    """Exists x in range(a) such that for all y in range(b), (x, y) in rel."""
    return any(all((x, y) in rel for y in range(b)) for x in range(a))

def forall_exists(rel, a, b):
    """For all y in range(b) there exists x in range(a) with (x, y) in rel."""
    return all(any((x, y) in rel for x in range(a)) for y in range(b))

def relations(a, b):
    """All relations between range(a) and range(b), as frozensets of pairs."""
    pairs = [(x, y) for x in range(a) for y in range(b)]
    return [frozenset(p for p, keep in zip(pairs, bits) if keep)
            for bits in itertools.product([False, True], repeat=len(pairs))]

def main():
    total = agree = 0
    for a in range(4):
        for b in range(1, 4):
            for f in functions(a, b):
                total += 1
                agree += preserves_intersections(f) == is_injective(f)
    print("1. f(S & T) = f(S) & f(T) for all S, T  <=>  f injective")
    print(f"   checked on all {total} functions between sets of size <= 3:"
          f" agrees in {agree}")
    f = (0, 0)
    s, t = frozenset({0}), frozenset({1})
    print(f"   smallest counterexample: f = {f}, S = {{0}}, T = {{1}}:")
    print(f"   f(S & T) = {set(image(f, s & t))},"
          f" f(S) & f(T) = {set(image(f, s) & image(f, t))}")
    print()
    bad_f = bad_g = 0
    example = None
    for a, b, c in itertools.product(range(1, 4), repeat=3):
        for f in functions(a, b):
            for g in functions(b, c):
                if is_injective(compose(g, f)):
                    bad_f += not is_injective(f)
                    if not is_injective(g):
                        bad_g += 1
                        example = example or (f, g)
    print("2. g o f injective: cases where f is not injective:", bad_f)
    print("   cases where g is not injective:", bad_g,
          f"(e.g. f = {example[0]}, g = {example[1]})")
    print()
    imp = conv = count = 0
    for a in range(1, 4):
        for b in range(1, 4):
            for rel in relations(a, b):
                count += 1
                ef, fe = exists_forall(rel, a, b), forall_exists(rel, a, b)
                imp += ef and not fe
                conv += fe and not ef
    print(f"3. all {count} relations between sets of size 1 to 3:")
    print(f"   exists-forall true but forall-exists false: {imp}")
    print(f"   forall-exists true but exists-forall false: {conv}")
    print("   e.g. P = equality on {0, 1}: every y has x = y, no x fits all")
    print()
    print("Epistemic status: exhaustive checks over finitely many small sets.")
    print("The counterexamples refute the general claims for good; the")
    print("agreements are evidence only. The general theorems are proved in")
    print("the lesson and in Lean (image_inter_of_injective, injective_of_comp,")
    print("exists_forall_imp).")

if __name__ == "__main__":
    main()

How small can a proof checker be? The second experiment implements one for a Hilbert-style system of propositional logic (two axiom schemes and modus ponens) in about twenty lines, checks the classic five-line proof of $p \to p$, and rejects a faulty proof with a precise message. Checking a proof is a single pass over its lines; finding a proof is a search. That asymmetry is why proof assistants pair a small kernel with powerful tactics.

"""A proof checker in twenty lines: why checking is easier than finding.

A proof assistant's kernel only *checks* proofs. To see how small a checker
can be, we implement one for a Hilbert-style system of propositional logic
with implication only: the axiom schemes K: A -> (B -> A) and
S: (A -> (B -> C)) -> ((A -> B) -> (A -> C)), and the rule modus ponens. We
check the classic five-line proof of p -> p, reject a faulty proof with a
precise message, and test soundness: every axiom instance and every proved
formula is a tautology (true under all truth assignments). Checking takes one
pass over the proof; *finding* a proof is a search that can grow
exponentially, which is why proof assistants combine a small kernel with
tactics that search.
"""

import itertools

def imp(a, b):
    """The formula a -> b."""
    return ("->", a, b)

def show(f):
    """Readable form of a formula."""
    if isinstance(f, str):
        return f
    return f"({show(f[1])} -> {show(f[2])})"

def axiom(name, *args):
    """Instance of axiom scheme K (two arguments) or S (three arguments)."""
    if name == "K" and len(args) == 2:
        a, b = args
        return imp(a, imp(b, a))
    if name == "S" and len(args) == 3:
        a, b, c = args
        return imp(imp(a, imp(b, c)), imp(imp(a, b), imp(a, c)))
    raise ValueError(f"unknown axiom {name} with {len(args)} arguments")

def derive(proof):
    """Formulas proved by each line; returns (lines, None) or (lines, error).

    A step is ("K", A, B), ("S", A, B, C), or ("MP", i, j): from line i
    (a formula A) and line j (the formula A -> B), conclude B.
    """
    lines = []
    for n, step in enumerate(proof, start=1):
        if step[0] in ("K", "S"):
            lines.append(axiom(*step))
        elif step[0] == "MP":
            i, j = step[1], step[2]
            if not (1 <= i < n and 1 <= j < n):
                return lines, f"line {n}: refers to a line not yet proved"
            a, ab = lines[i - 1], lines[j - 1]
            if isinstance(ab, str) or ab[1] != a:
                return lines, (f"line {n}: line {j} does not have the form"
                               f" (line {i}) -> ...")
            lines.append(ab[2])
        else:
            return lines, f"line {n}: unknown rule {step[0]!r}"
    return lines, None

def check(proof, goal):
    """Check that `proof` is a correct proof of `goal`: (True, '') or (False, reason)."""
    lines, error = derive(proof)
    if error:
        return False, error
    if not lines or lines[-1] != goal:
        return False, "the last line is not the goal"
    return True, ""

def atoms(f):
    """The set of propositional variables in a formula."""
    return {f} if isinstance(f, str) else atoms(f[1]) | atoms(f[2])

def evaluate(f, val):
    """Truth value of a formula under a dict of truth values."""
    if isinstance(f, str):
        return val[f]
    return (not evaluate(f[1], val)) or evaluate(f[2], val)

def is_tautology(f):
    """True if f is true under every assignment to its variables."""
    names = sorted(atoms(f))
    return all(evaluate(f, dict(zip(names, vals)))
               for vals in itertools.product([False, True], repeat=len(names)))

P_IMP_P = [
    ("S", "p", imp("p", "p"), "p"),
    ("K", "p", imp("p", "p")),
    ("MP", 2, 1),
    ("K", "p", "p"),
    ("MP", 4, 3),
]

def main():
    goal = imp("p", "p")
    print("Checking the proof of p -> p:")
    lines, _ = derive(P_IMP_P)
    for n, (step, formula) in enumerate(zip(P_IMP_P, lines), start=1):
        rule = f"MP {step[1]},{step[2]}" if step[0] == "MP" else step[0]
        print(f"  {n}. {show(formula):44s} [{rule}]")
    print("  verdict:", check(P_IMP_P, goal))
    bad = P_IMP_P[:3] + [("MP", 1, 3)]
    print("A faulty proof (modus ponens on the wrong lines):")
    print("  verdict:", check(bad, goal))
    print()
    forms = ["p", "q", imp("p", "q"), imp("q", "p")]
    instances = [axiom("K", a, b) for a in forms for b in forms]
    instances += [axiom("S", a, b, c) for a in forms for b in forms
                  for c in forms]
    print(f"Soundness evidence: {len(instances)} axiom instances checked,"
          f" all tautologies: {all(map(is_tautology, instances))}")
    print("p -> p is a tautology:", is_tautology(goal))
    print("Peirce's law ((p -> q) -> p) -> p is a tautology:",
          is_tautology(imp(imp(imp("p", "q"), "p"), "p")))
    print("(it is not provable from K and S alone: they give only")
    print("intuitionistic implicational logic)")
    print()
    print("Epistemic status: the verdicts are exact computations. The")
    print("tautology checks are exhaustive over truth assignments but cover")
    print("only the axiom instances listed, so they are evidence for the")
    print("soundness theorem, which is proved by induction on proofs.")

if __name__ == "__main__":
    main()

A truth table settles a propositional formula by checking every assignment — a decision procedure, exactly what Lean's decide tactic does for finite questions. Peirce's law $((p \to q) \to p) \to p$ is a tautology, so classical logic proves it; but it cannot be derived from the axiom schemes K and S used in the second experiment, which capture only intuitionistic implication. In Lean, proving it requires classical reasoning (by_cases, ultimately Classical.choice). Compare it with the law of excluded middle below, and try your own formulas.

• Pioneers. Nicolaas Govert de Bruijn began the Automath project in Eindhoven in 1967; by 1977 L. S. van Benthem Jutting had checked all of Edmund Landau's Grundlagen der Analysis in it. In Poland Andrzej Trybulec started Mizar in 1973, whose Mathematical Library is still one of the largest. Robin Milner's LCF (Stanford and Edinburgh, 1970s) introduced the idea of theorems as an abstract type that only the kernel's rules can create, and the programming language ML to go with it; its descendants include HOL (Mike Gordon), HOL Light (John Harrison) and Isabelle (Lawrence Paulson, 1986).
• Type theory. Per Martin-Löf's intuitionistic type theory (1970s) and Thierry Coquand and Gérard Huet's calculus of constructions (1984–88) led to Coq (now called Rocq), developed in France from 1989. Georges Gonthier and colleagues used it to check the Four Colour Theorem (2005) and the Feit–Thompson odd order theorem (2012).
• Landmarks. Thomas Hales's Flyspeck project completed a formal proof of the Kepler conjecture in 2014. Lean was launched by Leonardo de Moura at Microsoft Research in 2013; Lean 4, with Sebastian Ullrich, appeared from 2021. The community library mathlib began in 2017 for Lean 3 and was ported to Lean 4 as Mathlib by 2023. The Liquid Tensor Experiment (2020–22) checked a frontier result of Clausen and Scholze, and in 2023 the proof of the polynomial Freiman–Ruzsa conjecture by Gowers, Green, Manners and Tao was formalised in Lean within about three weeks of its announcement. Kevin Buzzard and Mohammad Pedramfar's Natural Number Game (2019) has introduced many students to Lean.

• Jeremy Avigad and Patrick Massot, Mathematics in Lean (online book, continually updated) — the standard introduction to formalising undergraduate mathematics with Mathlib.
• Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4 (online book) — Lean's logic, tactics and type classes in detail.
• The mathlib Community, "The Lean mathematical library", Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020).
• Rob Nederpelt and Herman Geuvers, Type Theory and Formal Proof: An Introduction (2014) — the type theory beneath proof assistants.
• John Harrison, Handbook of Practical Logic and Automated Reasoning (2009) — decision procedures, proof search and the design of LCF-style provers.
• Kevin Buzzard and Mohammad Pedramfar, The Natural Number Game (2019) — an interactive first encounter with Lean.

Next in the Lumenary: type theory and propositions as types, formal methods and formalising published mathematics.