Infinitude of Primes - Goldbach's Proof

Goldbach proved the infinitude of primes by establishing that the Fermat numbers are pairwise prime. Aigner and Ziegler wrote down the proof as follows.

Proof. Let us first look at the Fermat numbers \(F_n = 2^{2^n} + 1\) for \(n = 0,1,2,\ldots\). We will show that any two Fermat numbers are relatively prime; hence there must be infinitely many primes. To this end, we verify the recursion \[ \prod_{k=0}^{n-1} F_k = F_n - 2 \quad (n \ge 1),\] from which our assertion follows immediately. Indeed, if \(m\) is a divisor of, say, \(F_k\) and \(F_n\) \((k < n)\), then \(m\) divides \(2\), and hence \(m = 1\) or \(2\). But \(m = 2\) is impossible since all Fermat numbers are odd. To prove the recursion we use induction on \(n\). For \(n = 1\) we have \(F_0 = 3\) and \(F_1 - 2 = 3\). With induction, we now conclude \[\begin{align*}\prod_{k=0}^{n} F_k &= \left(\prod_{k=0}^{n-1} F_k \right) F_{n} = (F_n - 2) F_n = \\ & = (2^{2^n}-1) (2^{2^n}+1) = 2^{2^{n+1}}-1 =F_{n+1}-2. \end{align*}\]

Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 3.

The first sentence “Let us first look at the Fermat numbers \(F_n = 2^{2^n} + 1\) for \(n = 0,1,2,\ldots\)” gives us a definition of the Fermat numbers, which is taken care of easily enough in Lean.

def F (n : ℕ) : ℕ := 2 ^ 2 ^ n + 1

Regarding the rest of the proof, there is a lot to unpack here. As before, it makes sense at this point to isolate exactly what specific statement of the infinitude of prime we are establishing here. “We will show that any two Fermat numbers are prime; hence there must be infinitely many primes” indicates that we will establish a lemma F_coprime that will be the decisive ingredient to the actual proof. The implied argument is as follows: the Fermat numbers “grow beyond all bounds” (as Aigner and Ziegler state prior to the proof) and since the sets of their prime divisors are disjoint, so do the primes. The most appropriate statement of the infinitude of prime should therefore probably read something like ∃ P : ℕ → ℕ, Injective P ∧ ∀ k, (P k).Prime, that is there is a function \(P: \mathbb{N} \to \mathbb{N}\) that is injective and the images of which are primes.

Before we take a look at the proof of this statement, let us establish a technical lemma stating that all Fermat numbers are at least \(2\), since this will be used in two separated places. Of course, since \(F_0 = 3\) and the Fermat numbers are strongly monotone increasing, we in fact have \(F_n \ge 3\) (which we could also derive from the fact that Fermat numbers are odd, as we will later show), but \(F_n \ge 2\) will be sufficient for our purposes.

lemma F_ge_two (n : ℕ) : F n ≥ 2 := Nat.le.step (Nat.le_self_pow (NeZero.ne (2 ^ n)) 2)

The infinitude of primes assuming that Fermat numbers are coprime

Let us now establish a proof for this version of infinitude_of_primes, assuming that we have already established our lemma F_coprime.

theorem infinitude_of_primes : ∃ P : ℕ → ℕ, Injective P ∧ ∀ k, (P k).Prime := by choose P P_prime P_dvd_fermat using fun n ↦ Nat.exists_prime_and_dvd (ne_of_gt (F_ge_two n))

We specifically construct the desired function \(P: \mathbb{N} \to \mathbb{N}\) by mapping each n to some prime divisor of \(F_n\). In order for such a prime divisor to exists, we had to satisfy Nat.exists_prime_and_dvd by explicitly providing it with a proof of the fact that \(F_n \ne 1\), which is derived easily enough from F_ge_two. This gives us P and the fact that its images are prime P_prime, so it only remains to show that \(P\) is injective.

have P_inj : Injective P := by intros m n Pm_eq_Pn by_contra m_ne_n have Pm_dvd_gcd : P m ∣ Nat.gcd (F m) (F n) := Nat.dvd_gcd (P_dvd_fermat m) (Pm_eq_Pn ▸ P_dvd_fermat n) have Pm_dvd_one : P m ∣ 1 := F_coprime m n m_ne_n ▸ Pm_dvd_gcd exact Nat.Prime.ne_one (P_prime m) (Nat.dvd_one.mp Pm_dvd_one)

We need to show that \(P(m) = P(n)\) implies that \(m = n\). We assume by_contra that \(m \neq n\) and argue that \(P(m) \mid \gcd (F_m, F_n)\), which is true since \(P(m) = P(n)\) and \(P(m)\) and \(P(n)\) are respectively defined as divisors of \(F_m\) and \(F_n\), and that therefore \(P(m) \mid 1\) (since F_coprime tells us that Fermat numbers are pairwise coprime) a contradiction to the fact that \(P(m)\) is prime! Using this we can now easily conclude the proof by explicitly stating the function \(P\) along with its properties.

exact ⟨P, P_inj, P_prime⟩

A product form for Fermat numbers

Having established the implied part of the proof, let us turn to the actual heart of it. In order to ultimately establish that Fermat numbers are pairwise coprime, “we verify the recursion \(\prod_{k=0}^{n-1} F_k = F_n - 2\)”. The formula can be expressed in Lean as follows:

lemma F_prod_form (n : ℕ) : (∏ k in range n, F k) = F n - 2 := by

Note that range n denotes all natural numbers less than \(n\), that is including \(0\) and excluding \(n\). “To prove the recursion we use induction on \(n\)” is taken care of through induction' n with n ih with the inductive base case (explicitly computed by Aigner and Ziegler through “For \(n = 1\) we have \(F_0 = 3\) and \(F_1 - 2 = 3\).”) taken care of through exact rfl. It should be noted that Aigner and Ziegler only state the product form for \(n \geq 1\) and hence their base case is \(n = 1\). We stated it for \(n \in \mathbb{N}\), which for Lean means that \(n = 0\) is possible. Letting the empty product to be equal \(1\), as Lean does, we see that the product form also holds in this case and hence our base case is \(n = 0\).

induction' n with n ih · exact rfl

It remains the inductive step, that, as Aigner and Ziegler do in their proof, we formulate as one calculation, that is we use the calc tactic in Lean. Unfortunately, unlike the human readable proof, we do not quite have the luxury of appealing to the readers knowledge of basic algebra and arithmetic for each step. Instead we have to specify that the first step splits up the last factor of the product through Finset.prod_range_succ F n, then use the inductive assumption through rw [ih] and finally concludes the last three steps through a mixture of rfl and some tedious explicit calculations.

· calc ∏ k in range (Nat.succ n), F k _ = (∏ k in range n, F k) * F n := Finset.prod_range_succ F n _ = (F n - 2) * F n := by rw [ih] _ = (2 ^ 2 ^ n - 1) * (2 ^ 2 ^ n + 1) := by exact rfl _ = 2 ^ (2 ^ Nat.succ n) - 1 := by simp [Nat.mul_sub_right_distrib, Nat.mul_add]; rw [tsub_add_tsub_cancel (Nat.le_mul_self (2 ^ 2 ^ n)) (Nat.one_le_two_pow (2 ^ n))]; rw [←Nat.pow_two, ←Nat.pow_mul', ←Nat.pow_succ'] _ = F (Nat.succ n) - 2 := by exact rfl

At this point it is important to remark on important technical detail, that perhaps also explains the slightly tedious proof for the step from (2 ^ 2 ^ n - 1) * (2 ^ 2 ^ n + 1) to 2 ^ (2 ^ Nat.succ n) - 1: we have exclusively worked in the natural numbers \(\mathbb{N}\). This means that whenever a minus sign is used (for example already for lemma F_prod_form) we in fact were not referring to the additive inverse element of a natural number in \(\mathbb{Z}\) but to Lean’s subtraction of two natural numbers that saturates at \(0\), meaning that \(a - b = 0\) whenever \(a,b \in \mathbb{N}\) and \(b \geq a\). Since we were in fact always dealing with the case \(a \ge b\) this was not an issue, but it did limit the kind of arguments we could invoke. A more streamlined approach could have consisted of casting the appropriate types to the integers and making use of tactics like linarith or ring (though Moritz Firsching managed to be more succinct in his version of the proof without explicit casting). We will cover this in future posts.

Having established the product form of the Fermat numbers, and before jumping into the proof of F_coprime, it’s worth having a look at the final conclusion of the proof, which derives a contradiction “since all Fermat numbers are odd”. We could establish this fact later within the proof of F_coprime, but it feels worthy of being its own lemma. Why exactly are the Fermat numbers odd? Because \(2^{2^n}\) obviously is even, established through (Nat.even_pow' (NeZero.ne (2 ^ n))).mpr (Nat.even_iff.mpr rfl), so \(2^{2^n} + 1\) must be odd, establish through Even.add_one.

lemma F_odd (n : ℕ) : Odd (F n) := Even.add_one ((Nat.even_pow' (NeZero.ne (2 ^ n))).mpr (Nat.even_iff.mpr rfl))

Establishing that fermat numbers are coprime

Let us finally look at the proof that Fermat numbers are indeed pairwise coprime. Mathlib sees two numbers as coprime iff their \(\gcd\) is one. This is also the form that we have used in our proof of infinitude_of_primes. The sensible approach as someone working in Lean would be to stay close to this definition and directly establish that the greatest common divisor is one. The proof we are following however has a slightly different understand of coprimality: “Indeed, if \(m\) is a divisor of, say, \(F_k\) and \(F_n\)”, which is lead to the conclusion that \(m = 1\), i.e., two numbers are coprime if any arbitrary divisor of both must be one. To allow us to switch between these two understandings of coprimality, we therefore establish the following lemma.

lemma coprime_iff_divisors_one (k n : ℕ) : Nat.Coprime k n ↔ ∀ m, m ∣ k ∧ m ∣ n → m = 1 := ⟨λ k_n_coprime _ ↦ (λ ⟨m_dvd_k, m_dvd_n⟩ ↦ Nat.eq_one_of_dvd_coprimes k_n_coprime m_dvd_k m_dvd_n), λ h ↦ h (Nat.gcd k n) ⟨Nat.gcd_dvd_left k n, Nat.gcd_dvd_right k n⟩⟩

This finally allows us to approach a proof of F_coprime in the form in which we have used it infinitude_of_primes, by immediately rewriting the goal into the form that Aigner and Ziegler pursue.

lemma F_coprime (k n : ℕ) (k_ne_n: k ≠ n) : Nat.Coprime (F k) (F n) := by rw [coprime_iff_divisors_one] intro m ⟨m_dvd_Fk, m_dvd_Fn⟩

As more of an aside, they also assume that w.l.o.g. “\((k < n)\)”. We can do the same, but we do need to be more explicit by also providing a proof of exactly why there is in fact no loss of generality.

wlog k_lt_n : k < n · exact this n k k_ne_n.symm m m_dvd_Fn m_dvd_Fk (lt_of_le_of_ne (le_of_not_gt k_lt_n) k_ne_n.symm)

Now the proof proceeds by stating that “\(m\) divides \(2\)”, which does in fact follow from the product form F_prod_form of the Fermat numbers along with the fact that a divisor of a factor of a product also divides the product (dvd_prod_of_mem).

· have m_dvd_two : m ∣ 2 := by rw [←Nat.sub_sub_self (F_ge_two n), ←F_prod_form] exact Nat.dvd_sub' m_dvd_Fn (Nat.dvd_trans m_dvd_Fk (dvd_prod_of_mem F (mem_range.mpr k_lt_n)))

Since \(m \mid 2\) (m_dvd_two), “\(m = 1\) or \(2\)”, which we express as \(m \ne 0\) and \(m \le 2\) (keep in mind that we are working in the natural numbers throughout).

have m_ne_zero : m ≠ 0 := ne_zero_of_dvd_ne_zero (Nat.succ_ne_zero 1) m_dvd_two have m_le_two : m ≤ 2 := Nat.le_of_dvd (Nat.two_pos) m_dvd_two

Finally, we conclude that “\(m = 2\) is impossible since all Fermat numbers are odd”, and this is indeed the place where F_odd makes its first and only occurrence.

have m_ne_two : m ≠ 2 := λ m_eq_two ↦ Nat.even_iff_not_odd.mp (even_iff_two_dvd.mpr (m_eq_two ▸ m_dvd_Fn)) (F_odd n) exact Nat.eq_of_lt_succ_of_not_lt (lt_of_le_of_ne m_le_two m_ne_two) (Nat.not_lt.mpr (Nat.one_le_iff_ne_zero.mpr m_ne_zero))

This concludes the proof. 🎉