The next proof takes an algebraic turn, deriving a contradiction from the assumption that there exists a largest prime through Lagrange’s theorem.

Proof. Suppose \(\mathbb{P}\) is finite and \(p\) is the largest prime. We consider the so-called Mersenne number \(2^p - 1\) and show that any prime factor \(q\) of \(2^p - 1\) is bigger than \(p\), which will yield the desired conclusion. Let \(q\) be a prime dividing \(2^p - 1\), so we have \(2^p \equiv 1 \: (\operatorname{mod} \, q)\). Since \(p\) is prime, this means that the element \(2\) has order \(p\) in the multiplicative group \(\mathbb{Z}_q \setminus \{0\}\) of the field \(\mathbb{Z}_q\). This group has \(q-1\) elements. By Lagrange's theorem [...] we know that the order of every element divides the size of the group, that is, we have \(p \mid q-1\) and hence \(p < q\).
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 4.

The sentence “consider the so-called Mersenne number \(2^p - 1\) and show that any prime factor \(q\) of \(2^p - 1\) is bigger than \(p\)” indicates that we first establish the following lemma, from which the actual infinitude of primes will later be derived.

1

lemma mersenne_prime_dvd_gt (p q : ℕ) [p_prime: Fact (Nat.Prime p)] [q_prime : Fact (Nat.Prime q)] (h : q ∣ 2^p - 1) : p < q := by

Note that Fact is simply a neat way of letting Lean infer an assumption when applying a statement, so that you can just call some_theorem p instead of some_theorem p p_prime. We will use several statements that will automatically infer the info that p and q are prime, but we will also encounter statements that want to be given this info explicitly, in which case we simply turn the Fact back into its underlying assumption through p_prime.out or, more explicitly, Fact.out p_prime. In order to create a fact from an assumption, one can use Fact.mk.

The assumptions [q_prime: Fact (Nat.Prime q)] and (h : q ∣ 2^p - 1) express “(l)et \(q\) be a prime dividing \(2^p - 1\)” and the consequence “we have \(2^p \equiv 1 \: (\operatorname{mod} \, q)\)” follows from Nat.modEq_iff_dvd'. The Nat indicates this lemma applies to natural numbers (rather than integers) and indeed the expression 2^p - 1 also referred to subtraction in the natural numbers that saturates at zero. Thankfully this is not a problem, since \(2^p \geq 1\) due to Nat.one_le_two_pow.

1

  have two_pow_p_eq_one_mod_q : 2^p ≡ 1 [MOD q] := ((λ x ↦ (Nat.modEq_iff_dvd' x).mpr) (Nat.one_le_two_pow) h).symm

Next up, the proof states that “(s)ince \(p\) is prime, this means that the element \(2\) has order \(p\) in the multiplicative group \(\mathbb{Z}_q \setminus \{0\}\) of the field \(\mathbb{Z}_q\).” Fortunately, the orderOf_eq_prime lemma in mathlib directly supports this argument.

1
2
3

  have two_pow_p_eq_one := ((ZMod.eq_iff_modEq_nat q).mpr two_pow_p_eq_one_mod_q)
  rw [Nat.cast_pow, Nat.cast_one] at two_pow_p_eq_one
  have order_two_eq_p := orderOf_eq_prime two_pow_p_eq_one (by apply sub_eq_zero.not.mp; norm_num)

There are some nuances here: the first is that orderOf_eq_prime also requires a proof that \(2 \ne 1\) in \(\mathbb{Z}_q\), which we take care of through (by apply sub_eq_zero.not.mp; norm_num). The second is that two_pow_p_eq_one_mod_q was a statement about natural numbers 2 and 1, but we need a statement that \(2^p = 1\) in \(\mathbb{Z}_q\). ZMod.eq_iff_modEq_nat takes us most of the way there, but it takes 2^p as an integer and casts it in its entirety to \(\mathbb{Z}_q\). This is expressed in the Infoview through ↑(2 ^ p). However, what we actually want is the p-th exponent of the element 2 in \(\mathbb{Z}_q\). Rewriting with Nat.cast_pow gives us exactly that and turns the ↑(2 ^ p) into an ↑2 ^ p. However, one tiny issue remains: mathlib right now does not understand that ↑1 is also the multiplicative unit of \(\mathbb{Z}_q\). This important for orderOf_eq_prime, so we rewrite ↑1 to 1 using Nat.cast_one.

The proof continues by stating that “(t)his group has \(q-1\) elements.” and “(b)y Lagrange’s theorem […] we know that the order of every element divides the size of the group, that is, we have \(p \mid q-1\)”. Thankfully we do not have to go all the way to Lagrange’s theorem, since there is a lemma in mathlib in the form of ZMod.orderOf_dvd_card_sub_one stating this very fact.1 We just again need to supply it with a small, easily overlooked detail: we must have \(2 \ne 0\) in \(\mathbb{Z}_q\) (two_ne_zero). This is of course the case as long as \(q \ne 2\), which somewhat cumbersomely derive from h : q ∣ 2^p - 1.

1
2
3
4
5
6
7

  have two_ne_zero : (2 : ZMod q) ≠ 0 := by
    by_contra contra
    have q_lq_two : q ≤ 2 := (Nat.Prime.dvd_factorial q_prime.out).mp ((ZMod.nat_cast_zmod_eq_zero_iff_dvd 2 q).mp contra)
    have q_gt_two : q > 2 := Nat.lt_of_le_of_ne (Nat.Prime.two_le q_prime.out) (Odd.ne_two_of_dvd_nat (Nat.Even.sub_odd (Nat.one_le_two_pow) ( even_iff_two_dvd.mpr (dvd_pow_self 2 (Nat.Prime.ne_zero p_prime.out))) (Exists.intro Nat.zero rfl)) h).symm
    exact (Nat.not_lt.mpr q_lq_two) q_gt_two
    
  have p_dvd_q_minus_1 : p ∣ (q - 1) := order_two_eq_p ▸ (ZMod.orderOf_dvd_card_sub_one two_ne_zero)

Finally, we conclude the proof of our main lemma by deriving that “\(p < q\)”.

1

  exact Nat.lt_of_le_pred (Nat.Prime.pos q_prime.out) (Nat.le_of_dvd (Nat.sub_pos_of_lt (Nat.Prime.two_le q_prime.out)) p_dvd_q_minus_1)

This however does not conclude the actual proof of the infinitude of primes. The proof simply suggests we “(s)uppose \(\mathbb{P}\) is finite and \(p\) is the largest prime” and use the previous lemma to derive a contradiction. Let us do just that! We start by defining P as the set of primes and supposing that it is finite using by_contra, which allows us to define p as its maximum

1
2
3
4
5
6
7
8

theorem infinitude_of_primes : { p : ℕ | Nat.Prime p}.Infinite := by
  by_contra contra
  have : Fintype { p : ℕ | Nat.Prime p} := Set.Finite.fintype (Set.not_infinite.mp contra)
  let P := { p : ℕ | Nat.Prime p}.toFinset
  let P_nonenmpty : P.Nonempty := (Set.nonempty_of_mem (Set.mem_toFinset.mpr Nat.prime_two))
  let p := Finset.max' P P_nonenmpty
  have p_in_P : p ∈ P := Finset.max'_mem P P_nonenmpty
  have p_prime : Nat.Prime p := by simp [P] at p_in_P; exact p_in_P

Using this, we let \(q\) be an arbitrary prime divisor of \(2^p-1\), after establishing that \(2^p - 1 \neq 1\) (two_pow_p_minus_one_ne_one), and apply mersenne_prime_dvd_gt to obtain the fact that \(q > p\).

1
2
3

  have two_pow_p_minus_one_ne_one : 2^p - 1 ≠ 1 := Nat.ne_of_gt (Nat.lt_sub_of_add_lt ((@Nat.size_le 2 p).mp (Nat.Prime.two_le p_prime)))
  let ⟨q, q_prime, q_dvd⟩ := Nat.exists_prime_and_dvd two_pow_p_minus_one_ne_one
  have q_gt_p : q > p := @mersenne_prime_dvd_gt p q (Fact.mk p_prime) (Fact.mk q_prime) q_dvd

But this is of course a contradiction, since \(p\) was the largest prime and \(q\) is prime, so we must also have \(q \leq p\).

1
2

  have q_lt_p : q ≤ p := Finset.le_max' P q (Set.mem_toFinset.mpr q_prime)
  exact Nat.lt_irrefl p (Nat.lt_of_lt_of_le q_gt_p q_lt_p)

This concludes the proof. 🎉

  1. If this feels like cheating, check out Moritz Firsching’s version of this proof which consciously uses mathlib’s version of Lagrange’s theorem. ↩