Skip to main content

Challenge 4: There are infinitely many prime numbers

Also available in:

Español

Prove that there are infinitely many prime numbers.

To do so, complete the following Lean 4 theory:

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime.Defs

open Nat

example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
  sorry

1. Proof in natural language

Let \(p\) be the smallest prime factor of \(n! + 1\). It suffices to prove that \(n ≤ p\) and that \(p\) is prime.

To prove that \(p\) is prime, by the lemma minFac_prime, it suffices to prove that \[ n! + 1 ≠ 1 \] Its proof is \begin{align} n ! > 0 &\Longrightarrow n ! + 1 > 1 \\ &\Longrightarrow n ! + 1 ≠ 1 \end{align}

To prove \(n ≤ p\) it suffices to prove that \[ n ≱ p \] Its proof is \begin{array}{rll} n ≥ p &\Longrightarrow p \mid n! & &\\ &\Longrightarrow p \mid 1 & &\text{[because \(p \mid n! + 1\)]} \\ &\Longrightarrow \text{False} & &\text{[because \(p\) is prime]} \\ \end{array}

2. Proofs in Lean 4

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime.Defs

open Nat

-- Proof 1
-- =======

example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
  set p := minFac (n !  + 1)
  have h1 : Nat.Prime p := by
    apply minFac_prime
    -- ⊢ n ! + 1 ≠ 1
    have h3 : n ! > 0     := factorial_pos n
    have h4 : n ! + 1 > 1 := Nat.lt_add_of_pos_left h3
    exact Nat.ne_of_gt h4
  use p
  -- ⊢ n ≤ p ∧ Nat.Prime p
  constructor
  . -- ⊢ n ≤ p
    apply le_of_not_ge
    -- ⊢ ¬n ≥ p
    intro h5
    -- h5 : n ≥ p
    -- ⊢ False
    have h6 : p ∣ n ! := dvd_factorial (minFac_pos _) h5
    have h7 : p ∣ 1   := (Nat.dvd_add_iff_right h6).mpr (minFac_dvd _)
    exact (Nat.Prime.not_dvd_one h1) h7
  . -- ⊢ Nat.Prime p
    exact h1

-- Proof 2
-- =======

lemma L1 (n : ℕ) : n ! + 1 ≠ 1 :=
  Nat.ne_of_gt (succ_lt_succ (factorial_pos n))

lemma L2 (n : ℕ) : Nat.Prime (minFac (n ! + 1)) :=
  minFac_prime (L1 n)

lemma L3 (n : ℕ) : n ≤ minFac (n ! + 1) :=
by
  by_contra h1
  -- h1 : ¬n ≤ minFac (n ! + 1)
  -- ⊢ False
  apply Nat.Prime.not_dvd_one (L2 n)
  -- ⊢ (n ! + 1).minFac ∣ 1
  have h2 : minFac (n ! + 1) ∣ n ! :=
    dvd_factorial (minFac_pos _) (le_of_not_ge h1)
  exact (Nat.dvd_add_iff_right h2).mpr (minFac_dvd _)

example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p :=
by
  use minFac (n ! + 1)
  -- ⊢ n ≤ (n ! + 1).minFac ∧ Nat.Prime (n ! + 1).minFac
  exact ⟨L3 n, L2 n⟩

-- Proof 3
-- =======

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

-- Lemmas used
-- ===========

variable (k m n : ℕ)
#check (Nat.Prime.not_dvd_one : Nat.Prime n → ¬n ∣ 1)
#check (Nat.dvd_add_iff_right : k ∣ m → (k ∣ n ↔ k ∣ m + n))
#check (Nat.lt_add_of_pos_left : 0 < k → n < k + n)
#check (Nat.ne_of_gt : k < n → n ≠ k)
#check (dvd_factorial : 0 < k → k ≤ n → k ∣ n !)
#check (exists_infinite_primes n : ∃ p, n ≤ p ∧ Nat.Prime p)
#check (factorial_pos n: n ! > 0)
#check (le_of_not_ge : ¬k ≥ n → k ≤ n)
#check (minFac_dvd n : minFac n ∣ n)
#check (minFac_pos n : 0 < minFac n)
#check (minFac_prime : n ≠ 1 → Nat.Prime (minFac n))
#check (succ_lt_succ : n < m → n + 1 < m + 1)

You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.

3. Collaborative solutions

Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:

  • Write your proof in live.lean-lang.org and check that it compiles without errors.
  • Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean
   -- your proof
```

Comments