Wieferich and Mirimanoff primes

A Wieferich prime satisfies 2^(p-1) ≡ 1 [MOD p²]; a Mirimanoff prime satisfies 3^(p-1) ≡ 1 [MOD p²]. As of 2025, the only known Wieferich primes are 1093 and 3511; the only known Mirimanoff primes are 11 and 1006003.

The main result wieferich_mirimanoff shows that no prime below 6000 is simultaneously Wieferich and Mirimanoff. This is used in miller_rabin_squarefree to rule out squarefree pseudoprimes below 36 million (to bases 2 and 3).

def Wieferich (p : ℕ) : Prop

Equations

• Wieferich p = (2 ^ (p - 1) ≡ 1 [MOD p ^ 2])

def Mirimanoff (p : ℕ) : Prop

Equations

• Mirimanoff p = (3 ^ (p - 1) ≡ 1 [MOD p ^ 2])

noncomputable def wieferichKR (p : ℕ) : Bool

Equations

• wieferichKR p = (powModTR 2 p.pred (p.pow 2)).beq 1

noncomputable def mirimanoffKR (p : ℕ) : Bool

Equations

• mirimanoffKR p = (powModTR 3 p.pred (p.pow 2)).beq 1

@[simp]

theorem wieferichKR_eq_true_iff (p : ℕ) (hp : p ≠ 1) : wieferichKR p = true ↔ Wieferich p

@[simp]

theorem wieferichKR_eq_false_iff (p : ℕ) (hp : p ≠ 1) : wieferichKR p = false ↔ ¬Wieferich p

@[simp]

theorem mirimanoffKR_eq_true_iff (p : ℕ) (hp : p ≠ 1) : mirimanoffKR p = true ↔ Mirimanoff p

@[simp]

theorem mirimanoffKR_eq_false_iff (p : ℕ) (hp : p ≠ 1) : mirimanoffKR p = false ↔ ¬Mirimanoff p

We check odd numbers up to 6000 in the classes 1%6 and 5%6

theorem wieferich_mirimanoff₁ (n : ℕ) : n < 6000 → n % 6 = 1 → (wieferichKR n).not'.or' (mirimanoffKR n).not' = true

theorem wieferich₅ (n : ℕ) : n < 6000 → n % 6 = 5 → (!wieferichKR n) = true

theorem Nat.Prime.mod_6 {p : ℕ} (hp : Prime p) (hp₂ : p ≠ 2) (hp₃ : p ≠ 3) : p % 6 = 1 ∨ p % 6 = 5

theorem wieferich_mirimanoff {p : ℕ} (hp : Nat.Prime p) (p_bound : p < 6000) : ¬2 ^ (p - 1) ≡ 1 [MOD p ^ 2] ∨ ¬3 ^ (p - 1) ≡ 1 [MOD p ^ 2]

theorem pow_eq_one_of_dvd {M : Type u_1} [Monoid M] {x : M} {m n : ℕ} (h₁ : x ^ m = 1) (h₂ : m ∣ n) : x ^ n = 1

theorem miller_rabin_squarefree {n : ℕ} (hn₀ : n ≠ 0) (hn : n < 36000000) (h₂ : 2 ^ (n - 1) ≡ 1 [MOD n]) (h₃ : 3 ^ (n - 1) ≡ 1 [MOD n]) {p : ℕ} (hp : Nat.Prime p) (hpn : p ^ 2 ∣ n) : False