Fermat numbers

The Fermat numbers are a sequence of natural numbers defined as Nat.fermatNumber n = 2^(2^n) + 1, for all natural numbers n.

Main theorems

• Nat.coprime_fermatNumber_fermatNumber: two distinct Fermat numbers are coprime.
• Nat.pepin_primality: For 0 < n, Fermat number Fₙ is prime if 3 ^ (2 ^ (2 ^ n - 1)) = -1 mod Fₙ
• fermat_primeFactors_one_lt: For 1 < n, Prime factors the Fermat number Fₙ are of form k * 2 ^ (n + 2) + 1.

def Nat.fermatNumber (n : ℕ) : ℕ

Fermat numbers: the n-th Fermat number is defined as 2^(2^n) + 1.

Equations

• n.fermatNumber = 2 ^ 2 ^ n + 1

@[simp]

theorem Nat.fermatNumber_zero : Nat.fermatNumber 0 = 3

@[simp]

theorem Nat.fermatNumber_one : Nat.fermatNumber 1 = 5

@[simp]

theorem Nat.fermatNumber_two : Nat.fermatNumber 2 = 17

theorem Nat.strictMono_fermatNumber : StrictMono Nat.fermatNumber

theorem Nat.two_lt_fermatNumber (n : ℕ) : 2 < n.fermatNumber

theorem Nat.odd_fermatNumber (n : ℕ) : Odd n.fermatNumber

theorem Nat.fermatNumber_product (n : ℕ) : ∏ k ∈ Finset.range n, k.fermatNumber = n.fermatNumber - 2

theorem Nat.fermatNumber_eq_prod_add_two (n : ℕ) : n.fermatNumber = ∏ k ∈ Finset.range n, k.fermatNumber + 2

theorem Nat.fermatNumber_succ (n : ℕ) : (n + 1).fermatNumber = (n.fermatNumber - 1) ^ 2 + 1

theorem Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq (n : ℕ) : 2 * (n.fermatNumber - 1) ^ 2 ≤ (n + 1).fermatNumber ^ 2

theorem Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) : (n + 2).fermatNumber = (n + 1).fermatNumber ^ 2 - 2 * (n.fermatNumber - 1) ^ 2

theorem Int.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) : ↑(n + 2).fermatNumber = ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2

theorem Nat.coprime_fermatNumber_fermatNumber {k n : ℕ} (h : k ≠ n) : n.fermatNumber.Coprime k.fermatNumber

Goldbach's theorem : no two distinct Fermat numbers share a common factor greater than one.

From a letter to Euler, see page 37 in [JW22].

theorem Nat.pow_of_pow_add_prime {a n : ℕ} (ha : 1 < a) (hn : n ≠ 0) (hP : Nat.Prime (a ^ n + 1)) : ∃ (m : ℕ), n = 2 ^ m

Prime a ^ n + 1 implies n is a power of two (Fermat primes).

theorem Nat.pepin_primality (n : ℕ) (h : 3 ^ 2 ^ (2 ^ n - 1) = -1) : Nat.Prime n.fermatNumber

Fₙ = 2^(2^n)+1 is prime if 3^(2^(2^n-1)) = -1 mod Fₙ (Pépin's test).

theorem Nat.pepin_primality' (n : ℕ) (h : 3 ^ ((n.fermatNumber - 1) / 2) = -1) : Nat.Prime n.fermatNumber

Fₙ = 2^(2^n)+1 is prime if 3^((Fₙ - 1)/2) = -1 mod Fₙ (Pépin's test).

theorem Nat.pow_pow_add_primeFactors_one_lt {a n p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hpdvd : p ∣ a ^ 2 ^ n + 1) : ∃ (k : ℕ), p = k * 2 ^ (n + 1) + 1

Prime factors of a ^ (2 ^ n) + 1 are of form k * 2 ^ (n + 1) + 1.

theorem Nat.fermat_primeFactors_one_lt (n p : ℕ) (hn : 1 < n) (hp : Nat.Prime p) (hpdvd : p ∣ n.fermatNumber) : ∃ (k : ℕ), p = k * 2 ^ (n + 2) + 1

Primality of Mersenne numbers Mₙ = a ^ n - 1

theorem Nat.prime_of_pow_sub_one_prime {a n : ℕ} (hn1 : n ≠ 1) (hP : Nat.Prime (a ^ n - 1)) : a = 2 ∧ Nat.Prime n

Prime a ^ n - 1 implies a = 2 and prime n.