Dave Ishii - Problem Solving Blog

This famous and elegant proof was discovered by the ancient Greek mathematician Euclid. It uses a method called proof by contradiction. This means we start by assuming the opposite of what we want to prove (i.e., we assume "there are only a finite number of primes") and then show that this assumption leads to a logical contradiction.

---

The Steps of the Proof

1. Assume There Is a Finite Number of Primes

Let's begin by assuming that the set of prime numbers is finite. If this is true, we can list all of them, from the first one to the very last one.

Let's call them:

Here, , , , and so on, until we reach the final prime, . Our assumption is that no other primes exist.

2. Construct a New Number

Next, let's create a new number, which we'll call . We'll construct by multiplying all the primes on our list together and then adding 1.

3. Analyze the Properties of P

Now, let's think about this number . What happens when we try to divide by any of the primes from our "complete" list ()?

• If we divide by , the part is perfectly divisible, but we are left with a remainder of 1.

• If we divide by , we get the same result: a remainder of 1.

• In fact, no matter which prime from our list we choose, dividing by it will always leave a remainder of 1.

This means that is not divisible by any of the prime numbers on our supposedly complete list.

4. The Contradiction

Here is where the problem arises. We know a fundamental rule about numbers: every integer greater than 1 is either a prime number itself or is divisible by at least one prime number.

Our number is clearly greater than 1. However, we've just shown that it's not divisible by any of the primes on our list. This leaves us with only two possibilities:

1. is itself a prime number. If this is true, we have found a new prime number that was not on our original list.

2. is a composite number (not prime). If this is true, it must be divisible by some prime number. But since it's not divisible by any prime on our list, it must be divisible by a new prime that wasn't on our list.

Both possibilities lead to the same conclusion: there must be another prime number that was not in our original list. This contradicts our initial assumption that we had listed all the prime numbers.

---

Conclusion

Since our initial assumption ("there is a finite number of primes") leads to a logical contradiction, the assumption must be false.

Therefore, there must be an infinite number of prime numbers. 🤓

(Copilot LEAN)

Here's a clean, well-commented Lean 4 formalization of Euclid's proof that there are infinitely many primes:

import Mathlib.Data.Nat.Prime

/-!
# Euclid's Theorem: Infinitely Many Primes

This file contains a formalization of Euclid's classical proof that 
there are infinitely many prime numbers, using proof by contradiction.
-/

open Nat

/-- 
Given any finite set of primes, we can construct a number that is 
either prime itself or divisible by a prime not in the set.
-/
theorem exists_prime_not_in_finset (s : Finset Nat) :
    ∃ p : Nat, p.Prime ∧ p ∉ s := by
  -- Construct P = (product of all numbers in s) + 1
  let P := (s.prod id) + 1
  
  -- P is greater than 1 (assuming s is nonempty; handles empty case too)
  have hP_pos : 1 < P := Nat.lt_succ_of_le (Finset.one_le_prod' (fun _ _ => zero_le _))
  
  -- By fundamental theorem: P has some prime divisor
  obtain ⟨p, hp_prime, hp_div⟩ := exists_prime_and_dvd hP_pos
  
  -- Show that p cannot be in s
  use p, hp_prime
  intro hp_in_s
  
  -- If p ∈ s, then p divides the product
  have hp_div_prod : p ∣ s.prod id := Finset.dvd_prod_of_mem _ hp_in_s
  
  -- But p also divides P = prod + 1
  -- So p divides P - prod = 1, which is impossible for a prime
  have hp_div_one : p ∣ 1 := by
    have : p ∣ P - s.prod id := Nat.dvd_sub' hp_div hp_div_prod
    simpa using this
  
  -- Contradiction: no prime divides 1
  exact Prime.not_dvd_one hp_prime hp_div_one

/--
**Euclid's Theorem**: There are infinitely many prime numbers.

Proof strategy: Assume finitely many primes exist. Multiply them all 
together and add 1. This new number is either prime (contradiction) 
or has a prime factor not in our list (contradiction).
-/
theorem infinitely_many_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ p.Prime := by
  intro n
  -- Consider the set of all primes ≤ n
  let s := (Finset.range (n + 1)).filter Nat.Prime
  
  -- By our lemma, there exists a prime p not in this set
  obtain ⟨p, hp_prime, hp_not_in_s⟩ := exists_prime_not_in_finset s
  
  use p, hp_prime
  
  -- Since p ∉ s and s contains all primes ≤ n, we have p > n
  by_contra h_le
  push_neg at h_le
  apply hp_not_in_s
  simp [s]
  exact ⟨h_le, hp_prime⟩

#check infinitely_many_primes
-- ∀ (n : ℕ), ∃ p, n < p ∧ p.Prime

/-! 
## Example usage
-/

-- There exists a prime greater than 100
example : ∃ p : Nat, 100 < p ∧ p.Prime := infinitely_many_primes 100

-- There exists a prime greater than 1000000
example : ∃ p : Nat, 1000000 < p ∧ p.Prime := infinitely_many_primes 1000000

Key features of this code:

1. Clear structure: Main theorem infinitely_many_primes with a helper lemma
2. Detailed comments: Explains the proof strategy at each step
3. Modern Lean 4 syntax: Uses by tactic blocks and structured proofs
4. Faithful to Euclid: Constructs P = (product) + 1 and shows it leads to contradiction
5. Examples: Demonstrates the theorem with concrete instances

The proof captures the essence of Euclid's argument: given any finite collection of primes, we can always find another one!

(AXIOMS)

Great question! Let's break down the foundational axioms and key definitions that Lean needs for this proof:

Core Lean Axioms (Type Theory Foundation)

Lean 4 is based on a variant of the Calculus of Inductive Constructions. For this proof, Lean uses these fundamental axioms:

-- 1. Propositional Extensionality
-- Two propositions are equal if they're logically equivalent
axiom propext {P Q : Prop} : (P ↔ Q) → P = Q

-- 2. Quotient Types (for defining equivalence relations)
axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, 
  r a b → Quot.mk r a = Quot.mk r b

-- 3. Axiom of Choice
-- If every type in a family is nonempty, we can pick an element from each
axiom Classical.choice {α : Sort u} : Nonempty α → α

-- 4. Function Extensionality (derivable from propext + quot, but often listed)
-- Two functions are equal if they give equal outputs for all inputs

What Must Be Well-Defined for Our Proof

1. Natural Numbers (ℕ) as an Inductive Type

-- Natural numbers are built inductively (not an axiom, but a definition)
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

2. Arithmetic Operations

-- Addition (defined recursively)
def Nat.add : Nat → Nat → Nat
  | a, 0     => a
  | a, b + 1 => (a + b) + 1

-- Multiplication (defined recursively)
def Nat.mul : Nat → Nat → Nat
  | a, 0     => 0
  | a, b + 1 => a * b + a

3. Divisibility

-- a divides b if there exists k such that b = a * k
def Nat.dvd (a b : Nat) : Prop := ∃ k, b = a * k

4. Prime Numbers

-- A prime is a natural > 1 that is only divisible by 1 and itself
def Nat.Prime (p : Nat) : Prop :=
  2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p

5. Fundamental Theorem: Every n > 1 Has a Prime Divisor

This is crucial for Euclid's proof and requires proof (not an axiom):

-- This is a THEOREM that must be proven from the definitions above
theorem exists_prime_and_dvd {n : Nat} (h : 1 < n) : 
  ∃ p, Prime p ∧ p ∣ n := by
  -- Proof by strong induction on n
  -- Base case: n = 2 is prime
  -- Inductive case: if n is composite, it has a proper divisor d,
  --   and by IH, d has a prime divisor which also divides n
  sorry

Detailed Breakdown for Euclid's Proof

Here's what we actually use in the proof:

Component	Type	Required For
Inductive types	Axiom	Defining ℕ itself
Recursion principle	Derived from inductive types	Defining +, ×, etc.
Propositional logic	Built-in	Proof by contradiction
Classical logic (LEM)	Axiom (via Classical.choice)	Proof by contradiction
Product of finset	Definition	Constructing P = (∏ primes) + 1
Divisibility properties	Theorems	Showing p ∣ prod and p ∣ P
Prime → ¬(p ∣ 1)	Theorem	Getting the contradiction
∃ prime divisor	Theorem (FTA)	Finding p that divides P

The Critical Theorem: Fundamental Theorem of Arithmetic (Light Version)

The most important non-obvious requirement is:

-- Every natural number > 1 has at least one prime divisor
theorem exists_prime_divisor {n : Nat} (h : 1 < n) : 
  ∃ p, Prime p ∧ p ∣ n

This isn't an axiom—it's proven by strong induction, which itself relies on:

• Well-foundedness of < on ℕ (derivable from the inductive definition)
• The principle of mathematical induction

Summary

Axioms needed:

1. ✅ Propositional extensionality
2. ✅ Quotient types
3. ✅ Classical logic (Law of Excluded Middle / Choice) - for proof by contradiction
4. ✅ Inductive types - for defining ℕ

Must be proven (not axiomatic):

• Arithmetic properties (+, ×, distributivity, etc.)
• Divisibility lemmas
• The existence of prime divisors (mini version of FTA)
• Prime numbers don't divide 1

The beauty of Lean is that almost everything except the core type theory is constructed rather than assumed! 🎯