Classic Proofs
This article presents proofs you likely encountered in undergraduate mathematics, now written in Lean. Each example shows the traditional proof and its formalization side by side. The goal is not to teach you these theorems; you already know them. The goal is to build intuition for how mathematical reasoning translates into Lean code. When you see a proof by contradiction in English, what tactic does that become? When a textbook says “by strong induction,” what does Lean require? The side-by-side format lets you map familiar reasoning patterns onto unfamiliar syntax.
Euclid’s proof of the infinitude of primes has survived for over two thousand years. It requires no calculus, no abstract algebra, only the observation that $n! + 1$ shares no prime factors with $n!$. Yet formalizing this argument reveals hidden assumptions: that every number greater than one has a prime divisor, that primes are well-defined, that contradiction is a valid proof technique. The proofs here are not difficult by mathematical standards, but they exercise the full machinery of dependent types, tactics, and theorem proving. If you can formalize theorems that have survived two millennia of scrutiny, how hard can proving your web app correctly validates email addresses really be?
Infinitude of Primes
Traditional Proof
Theorem. There exist infinitely many prime numbers.
The proof proceeds in two parts. First, we establish that every integer $n \geq 2$ has a prime divisor. If $n$ is prime, it divides itself. Otherwise, $n$ has a proper divisor $m$ with $1 < m < n$. By strong induction, $m$ has a prime divisor $p$, and since $p \mid m$ and $m \mid n$, we have $p \mid n$.
Second, we show that for any $n$, there exists a prime $p > n$. Consider $N = n! + 1$. Since $n! \geq 1$, we have $N \geq 2$, so $N$ has a prime divisor $p$. We claim $p > n$. Suppose for contradiction that $p \leq n$. Then $p \mid n!$ since $n!$ contains all factors from 1 to $n$. Since $p \mid N$ and $p \mid n!$, we have $p \mid (N - n!) = 1$. But $p \geq 2$, so $p \nmid 1$, a contradiction. Therefore $p > n$. QED
Lean Formalization
The Lean proof mirrors this structure exactly. The theorem exists_prime_factor establishes the first part by case analysis and strong induction (via termination_by). The main theorem InfinitudeOfPrimes constructs $n! + 1$, extracts a prime divisor, then derives a contradiction using dvd_factorial and Nat.dvd_add_right.
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic
namespace ZeroToQED.Proofs
open Nat
theorem exists_prime_factor (n : ℕ) (hn : 2 ≤ n) : ∃ p, Nat.Prime p ∧ p ∣ n := by
by_cases hp : Nat.Prime n
· exact ⟨n, hp, dvd_refl n⟩
· obtain ⟨m, hm_dvd, hm_ne_one, hm_ne_n⟩ := exists_dvd_of_not_prime hn hp
have hm_lt : m < n := lt_of_le_of_ne (Nat.le_of_dvd (by omega) hm_dvd) hm_ne_n
have hm_ge : 2 ≤ m := by
rcases m with _ | _ | m <;> simp_all
obtain ⟨p, hp_prime, hp_dvd⟩ := exists_prime_factor m hm_ge
exact ⟨p, hp_prime, dvd_trans hp_dvd hm_dvd⟩
termination_by n
theorem factorial_pos (n : ℕ) : 0 < n ! := Nat.factorial_pos n
theorem dvd_factorial {k n : ℕ} (hk : 0 < k) (hkn : k ≤ n) : k ∣ n ! :=
Nat.dvd_factorial hk hkn
theorem InfinitudeOfPrimes : ∀ n, ∃ p > n, Nat.Prime p := by
intro n
have hN : 2 ≤ n ! + 1 := by
have hfact : 0 < n ! := factorial_pos n
omega
obtain ⟨p, hp_prime, hp_dvd⟩ := exists_prime_factor (n ! + 1) hN
refine ⟨p, ?_, hp_prime⟩
by_contra hle
push_neg at hle
have hp_pos : 0 < p := hp_prime.pos
have hdvd_fact : p ∣ n ! := dvd_factorial hp_pos hle
have hdvd_one : p ∣ 1 := (Nat.dvd_add_right hdvd_fact).mp hp_dvd
have hp_le_one : p ≤ 1 := Nat.le_of_dvd one_pos hdvd_one
have hp_ge_two : 2 ≤ p := hp_prime.two_le
omega
end ZeroToQED.Proofs
Alternative: Proof by Grind
The same theorem admits a much shorter proof using Lean’s grind tactic. The proof below defines its own IsPrime predicate and factorial to remain self-contained. Notice how each theorem body collapses to one or two lines, with grind handling the case analysis and arithmetic that required explicit by_contra, push_neg, and omega calls in the manual version.
import Mathlib.Tactic
namespace ZeroToQED.Proofs.Grind
/-- A prime is a number larger than 1 with no trivial divisors -/
def IsPrime (n : Nat) := 1 < n ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n
/-- Every number larger than 1 has a prime factor -/
theorem exists_prime_factor :
∀ n, 1 < n → ∃ k, IsPrime k ∧ k ∣ n := by
intro n h1
by_cases hprime : IsPrime n
· grind [Nat.dvd_refl]
· obtain ⟨k, _⟩ : ∃ k, 1 < k ∧ k < n ∧ k ∣ n := by
simp_all [IsPrime]
obtain ⟨p, _, _⟩ := exists_prime_factor k (by grind)
grind [Nat.dvd_trans]
/-- The factorial, defined recursively -/
def factorial : Nat → Nat
| 0 => 1
| n+1 => (n + 1) * factorial n
/-- Factorial postfix notation -/
notation:10000 n "!" => factorial n
/-- The factorial is always positive -/
theorem factorial_pos : ∀ n, 0 < n ! := by
intro n; induction n <;> grind [factorial]
/-- The factorial is divided by its constituent factors -/
theorem dvd_factorial : ∀ n, ∀ k ≤ n, 0 < k → k ∣ n ! := by
intro n; induction n <;>
grind [Nat.dvd_mul_right, Nat.dvd_mul_left_of_dvd, factorial]
/-- There are infinitely many primes: for any n, there exists p > n that is prime -/
theorem InfinitudeOfPrimes : ∀ n, ∃ p > n, IsPrime p := by
intro n
have : 1 < n ! + 1 := by grind [factorial_pos]
obtain ⟨p, hp, _⟩ := exists_prime_factor (n ! + 1) this
suffices ¬p ≤ n by grind
intro (_ : p ≤ n)
have : 1 < p := hp.1
have : p ∣ n ! := dvd_factorial n p ‹p ≤ n› (by grind)
have := Nat.dvd_sub ‹p ∣ n ! + 1› ‹p ∣ n !›
grind [Nat.add_sub_cancel_left, Nat.dvd_one]
end ZeroToQED.Proofs.Grind
Both proofs establish the same theorem. The explicit version teaches you the proof structure; the grind version shows what automation can handle once you understand the underlying mathematics.
Irrationality of $\sqrt{2}$
Traditional Proof
Theorem. $\sqrt{2}$ is irrational.
The key lemma is: if $n^2$ is even, then $n$ is even. We prove the contrapositive. Suppose $n$ is odd, so $n = 2k + 1$ for some integer $k$. Then $n^2 = (2k+1)^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$, which is odd. Therefore, if $n^2$ is even, $n$ cannot be odd, so $n$ must be even.
Now suppose $\sqrt{2} = p/q$ where $p, q$ are integers with $q \neq 0$ and $\gcd(p,q) = 1$. Then $2q^2 = p^2$, so $p^2$ is even, hence $p$ is even. Write $p = 2k$. Then $2q^2 = 4k^2$, so $q^2 = 2k^2$, meaning $q^2$ is even, hence $q$ is even. But then $\gcd(p,q) \geq 2$, contradicting our assumption. QED
Lean Formalization
The Lean code proves the parity lemmas explicitly. The theorem sq_odd_of_odd shows that squaring an odd number yields an odd number by expanding $(2k+1)^2$. The theorem even_of_sq_even proves the contrapositive: assuming $n$ is odd leads to $n^2$ being odd, which contradicts $n^2$ being even. The final irrationality result follows from Mathlib’s irrational_sqrt_two, which uses this same parity argument internally.
import Mathlib.RingTheory.Real.Irrational
import Mathlib.Tactic
namespace ZeroToQED.Proofs
theorem sq_even_of_even {n : ℤ} (h : Even n) : Even (n ^ 2) := by
obtain ⟨k, hk⟩ := h
exact ⟨2 * k ^ 2, by rw [hk]; ring⟩
theorem sq_odd_of_odd {n : ℤ} (h : Odd n) : Odd (n ^ 2) := by
obtain ⟨k, hk⟩ := h
exact ⟨2 * k ^ 2 + 2 * k, by rw [hk]; ring⟩
theorem even_of_sq_even {n : ℤ} (h : Even (n ^ 2)) : Even n := by
by_contra hodd
rw [Int.not_even_iff_odd] at hodd
have hsq_odd : Odd (n ^ 2) := sq_odd_of_odd hodd
obtain ⟨k, hk⟩ := hsq_odd
obtain ⟨m, hm⟩ := h
omega
theorem sqrt2_irrational : Irrational (Real.sqrt 2) := irrational_sqrt_two
end ZeroToQED.Proofs
Euclid’s Lemma
Traditional Proof
Theorem (Euclid’s Lemma). If a prime $p$ divides a product $ab$, then $p \mid a$ or $p \mid b$.
Let $p$ be prime with $p \mid ab$. Since $p$ is prime, the only divisors of $p$ are 1 and $p$. Therefore $\gcd(p, a) \in \{1, p\}$ (greatest common divisor).
Case 1: If $\gcd(p, a) = p$, then $p \mid a$ and we are done.
Case 2: If $\gcd(p, a) = 1$, we show $p \mid b$. Consider $\gcd(pb, ab)$. Since $p \mid pb$ and $p \mid ab$, we have $p \mid \gcd(pb, ab)$. By the property $\gcd(pb, ab) = b \cdot \gcd(p, a) = b \cdot 1 = b$, we conclude $p \mid b$. QED
Lean Formalization
The Lean proof follows this GCD-based argument directly. It case-splits on whether $\gcd(p, a) = 1$ or $\gcd(p, a) > 1$. In the coprime case, it uses Nat.gcd_mul_right to establish that $\gcd(pb, ab) = b$, then shows $p$ divides this GCD. In the non-coprime case, since $p$ is prime, $\gcd(p, a) = p$, so $p \mid a$.
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Tactic
namespace ZeroToQED.Proofs
open Nat
theorem euclid_lemma {a b p : ℕ} (hp : Nat.Prime p) (h : p ∣ a * b) :
p ∣ a ∨ p ∣ b := by
rcases Nat.eq_or_lt_of_le (Nat.one_le_iff_ne_zero.mpr (Nat.gcd_pos_of_pos_left a hp.pos).ne')
with hcop | hncop
· right
have key : p ∣ Nat.gcd (p * b) (a * b) := Nat.dvd_gcd (dvd_mul_right p b) h
rwa [Nat.gcd_mul_right, hcop.symm, one_mul] at key
· left
have hdvd := Nat.gcd_dvd_left p a
rcases hp.eq_one_or_self_of_dvd _ hdvd with h1 | hp_eq
· omega
· have : p ∣ a := by rw [← hp_eq]; exact Nat.gcd_dvd_right p a
exact this
theorem prime_divides_product_iff {p a b : ℕ} (hp : Nat.Prime p) :
p ∣ a * b ↔ p ∣ a ∨ p ∣ b :=
⟨euclid_lemma hp, fun h => h.elim (dvd_mul_of_dvd_left · b) (dvd_mul_of_dvd_right · a)⟩
end ZeroToQED.Proofs
Binomial Theorem
Traditional Proof
Theorem (Binomial Theorem). For real numbers $x, y$ and natural number $n$: \[(x + y)^n = \sum_{k=0}^{n} \binom{n}{k} x^k y^{n-k}\]
The proof proceeds by induction. The base case $n = 0$ gives $(x+y)^0 = 1 = \binom{0}{0}x^0y^0$. For the inductive step, we expand $(x+y)^{n+1} = (x+y)(x+y)^n$, distribute, and apply Pascal’s identity $\binom{n}{k} + \binom{n}{k-1} = \binom{n+1}{k}$ to combine terms.
As concrete examples: $(x+1)^2 = x^2 + 2x + 1$ and $(x+1)^3 = x^3 + 3x^2 + 3x + 1$. QED
Lean Formalization
Mathlib provides add_pow, which establishes the binomial theorem via the same inductive argument. Our binomial_theorem reformulates this in the standard notation. The specific cases binomial_two and binomial_three are verified by the ring tactic, which normalizes polynomial expressions.
import Mathlib.Tactic
namespace ZeroToQED.Proofs
theorem binomial_theorem (x y : ℝ) (n : ℕ) :
(x + y) ^ n = (Finset.range (n + 1)).sum fun k => ↑(n.choose k) * x ^ k * y ^ (n - k) := by
rw [add_pow]
apply Finset.sum_congr rfl
intros k _
ring
theorem binomial_two (x : ℝ) : (x + 1) ^ 2 = x ^ 2 + 2 * x + 1 := by ring
theorem binomial_three (x : ℝ) : (x + 1) ^ 3 = x ^ 3 + 3 * x ^ 2 + 3 * x + 1 := by ring
example : (2 : ℝ) ^ 5 = 32 := by norm_num
end ZeroToQED.Proofs
Fibonacci Numbers
Traditional Proof
Definition. The Fibonacci sequence: $F_0 = 0$, $F_1 = 1$, $F_{n+2} = F_{n+1} + F_n$. The sequence that appears everywhere: rabbit populations, sunflower spirals, financial markets, bad interview questions.
Theorem. $\sum_{k=0}^{n-1} F_k + 1 = F_{n+1}$
Base case ($n = 0$): The empty sum equals 0, and $0 + 1 = 1 = F_1$.
Inductive step: Assume $\sum_{k=0}^{n-1} F_k + 1 = F_{n+1}$. Then: \[\sum_{k=0}^{n} F_k + 1 = \left(\sum_{k=0}^{n-1} F_k + 1\right) + F_n = F_{n+1} + F_n = F_{n+2}\] which equals $F_{(n+1)+1}$. QED
Lean Formalization
The Lean proof follows the same structure. The definition fib uses pattern matching on 0, 1, and $n+2$. The theorem fib_sum proceeds by induction: the base case simplifies directly, and the inductive step uses Finset.sum_range_succ to split off the last term, applies the inductive hypothesis, then uses the recurrence relation.
import Mathlib.Tactic
namespace ZeroToQED.Proofs
def fib : ℕ → ℕ
| 0 => 0
| 1 => 1
| n + 2 => fib (n + 1) + fib n
theorem fib_add_two (n : ℕ) : fib (n + 2) = fib (n + 1) + fib n := rfl
theorem fib_pos {n : ℕ} (h : 0 < n) : 0 < fib n := by
cases n with
| zero => contradiction
| succ n =>
cases n with
| zero => decide
| succ m =>
rw [fib_add_two]
exact Nat.add_pos_left (fib_pos (Nat.zero_lt_succ _)) _
theorem fib_sum (n : ℕ) : (Finset.range n).sum fib + 1 = fib (n + 1) := by
induction n with
| zero => simp [fib]
| succ n ih =>
rw [Finset.sum_range_succ, add_assoc, add_comm (fib n) 1, ← add_assoc, ih]
rfl
end ZeroToQED.Proofs
Pigeonhole Principle
Traditional Proof
Theorem (Pigeonhole Principle). Let $f : A \to B$ be a function between finite sets with $|A| > |B|$. Then $f$ is not injective: there exist distinct $a_1, a_2 \in A$ with $f(a_1) = f(a_2)$.
Suppose for contradiction that $f$ is injective, meaning $f(a_1) = f(a_2)$ implies $a_1 = a_2$. An injective function from $A$ to $B$ implies $|A| \leq |B|$, since distinct elements of $A$ map to distinct elements of $B$. But we assumed $|A| > |B|$, a contradiction. Therefore $f$ is not injective, so there exist distinct $a_1 \neq a_2$ with $f(a_1) = f(a_2)$. QED
Corollary. In any group of $n > 365$ people, at least two share a birthday.
Lean Formalization
The Lean proof mirrors this argument precisely. It assumes by contradiction (by_contra hinj) that no two distinct elements collide. The push_neg tactic transforms this into: for all $a_1, a_2$, if $a_1 \neq a_2$ then $f(a_1) \neq f(a_2)$. This is exactly injectivity. We then apply Fintype.card_le_of_injective, which states that an injective function implies $|A| \leq |B|$, contradicting our hypothesis $|B| < |A|$.
import Mathlib.Data.Fintype.Card
import Mathlib.Tactic
namespace ZeroToQED.Proofs
theorem pigeonhole {α β : Type*} [Fintype α] [Fintype β]
(f : α → β) (h : Fintype.card β < Fintype.card α) :
∃ a₁ a₂ : α, a₁ ≠ a₂ ∧ f a₁ = f a₂ := by
by_contra hinj
push_neg at hinj
have inj : Function.Injective f := fun a₁ a₂ heq =>
Classical.byContradiction fun hne => hinj a₁ a₂ hne heq
exact Nat.not_lt.mpr (Fintype.card_le_of_injective f inj) h
theorem birthday_pigeonhole {n : ℕ} (hn : 365 < n) (birthday : Fin n → Fin 365) :
∃ i j : Fin n, i ≠ j ∧ birthday i = birthday j := by
have hcard : Fintype.card (Fin 365) < Fintype.card (Fin n) := by simp [hn]
exact pigeonhole birthday hcard
end ZeroToQED.Proofs
Divisibility
Traditional Proof
Definition. We write $a \mid b$ (divisibility) if there exists $k$ such that $b = ak$.
Theorem. Divisibility satisfies:
- $a \mid a$ (reflexivity)
- $a \mid b \land b \mid c \Rightarrow a \mid c$ (transitivity)
- $a \mid b \land a \mid c \Rightarrow a \mid (b + c)$
- $a \mid b \Rightarrow a \mid bc$
Proof. (1) $a = a \cdot 1$, so take $k = 1$.
(2) If $b = ak$ and $c = bm$, then $c = (ak)m = a(km)$.
(3) If $b = ak$ and $c = am$, then $b + c = ak + am = a(k + m)$.
(4) If $b = ak$, then $bc = (ak)c = a(kc)$. QED
Lean Formalization
Each Lean proof constructs the witness $k$ explicitly. The obtain tactic extracts the witnesses from divisibility hypotheses, then we provide the new witness as an anonymous constructor ⟨_, _⟩. The equality proofs use rw to substitute and mul_assoc or mul_add to rearrange.
import Mathlib.Tactic
namespace ZeroToQED.Proofs
example : 3 ∣ 12 := ⟨4, rfl⟩
example : ¬5 ∣ 12 := by decide
theorem dvd_refl' (n : ℕ) : n ∣ n := ⟨1, (mul_one n).symm⟩
theorem dvd_trans' {a b c : ℕ} (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := by
obtain ⟨k, hk⟩ := hab
obtain ⟨m, hm⟩ := hbc
exact ⟨k * m, by rw [hm, hk, mul_assoc]⟩
theorem dvd_add' {a b c : ℕ} (hab : a ∣ b) (hac : a ∣ c) : a ∣ b + c := by
obtain ⟨k, hk⟩ := hab
obtain ⟨m, hm⟩ := hac
exact ⟨k + m, by rw [hk, hm, mul_add]⟩
theorem dvd_mul_right' (a b : ℕ) : a ∣ a * b := ⟨b, rfl⟩
theorem dvd_mul_left' (a b : ℕ) : b ∣ a * b := ⟨a, (mul_comm b a).symm⟩
end ZeroToQED.Proofs
Generalized Riemann Hypothesis
The proofs above are solved problems. But what about the unsolved ones? The Generalized Riemann Hypothesis asserts that all non-trivial zeros of Dirichlet L-functions have real part $\frac{1}{2}$. It has resisted proof since 1859. The statement is precise enough to formalize:
/-- The **Generalized Riemann Hypothesis** asserts that all the non-trivial zeros of the
Dirichlet L-function L(χ, s) of a primitive Dirichlet character χ have real part 1/2. -/
theorem generalized_riemann_hypothesis (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
(hχ : χ.IsPrimitive) (s : ℂ) (hs : χ.LFunction s = 0)
(hs_nontrivial : s ∉ Int.cast '' trivialZeros χ) :
s.re = 1 / 2 :=
sorry
That sorry is worth a million dollars from the Clay Mathematics Institute, a Fields Medal, arguably a Nobel Prize in Physics (for its implications in quantum chaos), a Turing Award if you use a computer to help, and mass adoration from strangers on the internet. The reward structure for closing that sorry is, by any reasonable measure, excessive.
Google DeepMind maintains a repository of open mathematical conjectures formalized in Lean, including the Generalized Riemann Hypothesis. The existence of this repository says something profound: the frontier of human mathematical knowledge can now be expressed as a list of sorry statements waiting to be filled. When someone eventually proves or disproves these conjectures, the proof will compile.