Case 2: Euclid: infinitely many primes🔗

Audit how a claim about infinity is stated, check a definition against its famous bugs, and read a classic proof.

The claim🔗

There are infinitely many prime numbers. Euclid proved it around 300 BC. It is one of the oldest theorems in mathematics, and Mathlib has it as Nat.exists_infinite_primes:

Nat.exists_infinite_primes : ∀ (n : ℕ), ∃ p, n ≤ p ∧ Nat.Prime p#check @Nat.exists_infinite_primes

Nat.exists_infinite_primes : ∀ (n : ℕ), ∃ p, n ≤ p ∧ Nat.Prime p

Notice: the claim says “infinitely many”, but the statement does not contain the word “infinite”. That is the first thing to check.

Step 1: does the statement say the claim?🔗

Statements that look close can be much weaker. Both of these are accepted by Lean, each with a one-line proof:

theorem only_one_prime : ∃ p, Nat.Prime p := ⟨2, Nat.prime_two⟩

theorem prime_below (n : ℕ) : ∃ p, p ≤ n + 2 ∧ Nat.Prime p := ⟨2, byn:ℕ⊢ 2 ≤ n + 2 omegaAll goals completed! 🐙, Nat.prime_two⟩

The first only says a prime exists. The second has the inequality the wrong way round, so the prime 2 works for every n. Neither says anything about infinity.

A second formalization is reassuring when two of them agree. Mathlib also states the claim literally, with the set of primes:

Nat.infinite_setOfPred_prime : {p | Nat.Prime p}.Infinite#check @Nat.infinite_setOfPred_prime

Nat.infinite_setOfPred_prime : {p | Nat.Prime p}.Infinite

“The set of primes is infinite.” Two different statements of the same claim, both proved in Mathlib.

Step 2: the definitions (checklist step 5)🔗

On Day 25 you saw an IsPrime that forgot “n ≥ 2” and so counted 1 as prime. Does Mathlib’s Nat.Prime have that bug?

def Nat.Prime : ℕ → Prop :=
fun p => Irreducible p#print Nat.Prime
@Nat.prime_def : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p#check @Nat.prime_def
example : Nat.Prime 7 := by⊢ Nat.Prime 7 decideAll goals completed! 🐙
example : ¬ Nat.Prime 1 := Nat.not_prime_one
example : ¬ Nat.Prime 0 := Nat.not_prime_zero

def Nat.Prime : ℕ → Prop :=
fun p => Irreducible p

@Nat.prime_def : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

#print shows Nat.Prime p is defined as Irreducible p, a general notion from algebra that is hard to read. But Mathlib proves Nat.prime_def, which restates it in school terms:

Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

And small cases behave: 7 is prime, 0 and 1 are not.

Steps 3 and 4: hypotheses, and step 1: axioms🔗

The statement has no hypotheses, only the variable n (“for every n”). Nothing to be vacuous, nothing circular.

'Nat.exists_infinite_primes' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms Nat.exists_infinite_primes

'Nat.exists_infinite_primes' depends on axioms: [propext, Classical.choice, Quot.sound]

Step 5: read the proof🔗

Euclid’s argument fits in a few lines. This is Mathlib’s proof, copied under a new name so it runs here:

open Nat in
theorem euclid (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p :=
  let p := minFac (n ! + 1)
  have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _
  have pp : Nat.Prime p := minFac_prime f1
  have np : n ≤ p :=
    le_of_not_ge fun h =>
      have h₁ : p ∣ n ! := dvd_factorial (minFac_pos _) h
      have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
      pp.not_dvd_one h₂
  ⟨p, np, pp⟩

Read it as a story:

Take the number n! + 1 (n factorial plus one: 1 · 2 · … · n + 1).
Let p be its smallest prime factor (minFac). It is prime (pp).
Why is p ≥ n (np)? Suppose p ≤ n. Then p is one of the factors of n!, so p divides n! (h₁). It also divides n! + 1, so it divides their difference, 1 (h₂). But no prime divides 1.

Try it on n = 4 with #eval:

25#eval Nat.factorial 4 + 1
5#eval Nat.minFac (Nat.factorial 4 + 1)

4! + 1 = 25, which is not prime, and its smallest prime factor is 5 ≥ 4. The proof finds the prime 5, not 25.