Infinitude of Primes – The Statement

This series of posts will be about the following simple statement.

Euclid's theorem. There are infinitely many prime numbers.

Our aim is to establish six distinct formal proofs based on the ones presented by Aigner and Ziegler in their book ‘Proofs from THE BOOK’. Before doing so, we first have to think about how exactly to even express a formal version of this statement. Perhaps the most straightforward interpretation simply states that { p : ℕ | Nat.Prime p}.Infinite, that is the set of all integers that are prime has infinite cardinality. However, this neither has to be the form in which will be most commonly applied nor the form in is most readily proven. In everyday usage we use these different forms interchangeably without a moments thought, but in Lean we don’t quite have that luxury, both when formalizing a proof and when using a statement.

We will in fact use one of several different variants for the six proofs, always choosing the one that is closest to the actual statement being made:

• One obvious alternate statement is (S : Finset ℕ) : ∃ p, Nat.Prime p ∧ p ∉ S, that is for any finite set of integers \(S\), we can find a natural number \(p\) that is prime and not in \(S\).
• Another version states that (S : Finset ℕ) (hS : ∀ s ∈ S, Nat.Prime s) : ∃ p, Nat.Prime p ∧ p ∉ S, that is for any finite set of primes (not just integers) \(S\), we can find a natural number \(p\) that is prime and not in \(S\). The assumption that the elements of \(S\) are prime can be convenient to have, but it is of course unnecessary, since we can easily establish the following equivalence to the previous statement.
• The version used in mathlib simply states (n : ℕ): ∃ p, Nat.Prime p ∧ p > n, that is for any natural number \(n\) we can find a prime \(p\) that is larger than \(n\). An equivalence to (S : Finset ℕ) : ∃ p, Nat.Prime p ∧ p ∉ S is of course again easily established, by letting either \(S = \{0, \ldots, n \}\) or \(n = \max S\) depending on the direction we are proving. The only significant detail to note is that for the latter, we need to treat the case \(S = \emptyset\) separately, as otherwise no maximum is defined.
• Finally, a perhaps less intuitive but still convenient version states ∃ (P : ℕ → ℕ), (Injective P) ∧ (∀ k, (P k).Prime), that is it establishes the existence of an injection \(P\) from the natural numbers to the primes.

All of these statements are of course equal, which the following statement establishes. We won’t go into details regarding these proofs, so feel free to skip them at this point if you are new to Lean, as they aren’t the most interesting proofs to get started with.

theorem infinitude_primes_tfae : List.TFAE [ { p : ℕ | Nat.Prime p}.Infinite, ∀ (S : Finset ℕ), (∃ p, Nat.Prime p ∧ p ∉ S), (∀ (S : Finset ℕ) (_ : ∀ s ∈ S, Nat.Prime s), (∃ p, Nat.Prime p ∧ p ∉ S)), (∀ n : ℕ, (∃ p, Nat.Prime p ∧ p > n)), ∃ (P : ℕ → ℕ), (Function.Injective P) ∧ (∀ k, (P k).Prime) ] := by tfae_have 1 ↔ 2 constructor · exact λ primes_are_infinite S ↦ Set.Infinite.exists_not_mem_finset primes_are_infinite S · intro rhs by_contra con simp [Set.Infinite] at con obtain ⟨p, ⟨p_prime, p_not_in_S⟩⟩ := rhs (Set.Finite.toFinset con) rw [Set.Finite.mem_toFinset con, Set.mem_setOf_eq] at p_not_in_S contradiction tfae_have 2 ↔ 3 constructor · exact fun a S _ ↦ a S · intro rhs S let Sprimes := S.filter Nat.Prime obtain ⟨p, p_prime, p_notin_Sprimes⟩ := rhs Sprimes (λ _ g ↦ (Finset.mem_filter.mp g).right) obtain p_notin_S := λ p_in_S ↦ p_notin_Sprimes (Finset.mem_filter.mpr ⟨p_in_S, p_prime⟩) exact ⟨p, ⟨p_prime, p_notin_S⟩⟩ tfae_have 4 ↔ 2 constructor · intro lhs S by_cases h : S.Nonempty · let S_max := Finset.max' S h obtain ⟨p, p_prime, p_gt_maxS⟩ := lhs S_max obtain p_notin_S := λ p_in_S ↦ LT.lt.false (Nat.lt_of_le_of_lt (Finset.le_max' S p p_in_S) p_gt_maxS ) exact ⟨p, ⟨p_prime, p_notin_S⟩⟩ · rw [Finset.not_nonempty_iff_eq_empty.mp h] exact ⟨2, Nat.prime_two, Finset.not_mem_empty 2⟩ · intro rhs n obtain ⟨p, p_prime, p_notin_S⟩ := rhs (Finset.range (n + 1)) have h : p > n := by simp [Finset.mem_range] at p_notin_S; exact p_notin_S exact ⟨p, ⟨p_prime, h⟩⟩ tfae_have 1 ↔ 5 constructor · let primes := { p : ℕ | Nat.Prime p} let P := λ n ↦ (Nat.nth (primes.Mem) n) exact λ h ↦ ⟨P, Nat.nth_injective h, λ k ↦ Nat.nth_mem_of_infinite h k⟩ · intro ⟨P, P_inj, P_im_prime⟩ exact Set.infinite_of_injective_forall_mem P_inj P_im_prime tfae_finish

Note that we can of course also establish that ‘TFAE’ through a simple cycle argument rather then a sequence of iff statements, as we have done here.