Primality tests in Lean
Main definitions
Fast modular exponentiation
/-- Fast modular exponentiation, tail recursive -/
def pow {n : ℕ} (x : ZMod n) (m : ℕ) : ZMod n
theorem pow_eq {n : ℕ} (x : ZMod n) (m : ℕ) :
x.pow m = x ^ m
Fermat probable primality
/-- `n` is a *Fermat probable prime* to base `a` if `a ^ (n - 1) = 1`. -/
def FPP (n : ℕ) (a : ZMod n) : Prop :=
a ^ (n - 1) = 1
instance FPP.decidable {n : ℕ} {a : ZMod n} :
Decidable (FPP n a)
/-- A prime is a Fermat probable prime to any nonzero base. -/
theorem FPP.of_prime {p : ℕ} [Fact p.Prime] {a : ZMod p} (ha : a ≠ 0) :
FPP p a
def FPP.Carmichael (n : ℕ) : Prop :=
∀ a : (ZMod n)ˣ, FPP n a
Strong probable primality
/-- `n` is a *strong probable prime* to base `a`, if `a ^ d = 1` or `∃ s < s', a ^ (2 ^ s * d) = -1`
where `d` is odd and `n - 1 = 2 ^ s' * d`. -/
def SPP (n : ℕ) (a : ZMod n) : Prop :=
a ^ oddPart (n - 1) = 1 ∨
∃ s : ℕ, s < val₂ (n - 1) ∧ a ^ (2 ^ s * oddPart (n - 1)) = -1
/-- The algorithm that decides `SPP` in $O(\log^3 n)$. -/
instance SPP.decidable {n : ℕ} {a : ZMod n} :
Decidable (SPP n a)
/-- A prime is a strong probable prime to any nonzero base. -/
theorem SPP.of_prime {p : ℕ} [Fact p.Prime] {a : ZMod p} (ha : a ≠ 0) :
SPP p a
/-- The proportion of Miller–Rabin nonwitnesses of composite `n` is at most 1/4. -/
theorem SPP.card_SPP_of_not_prime {n : ℕ} [hn : n.AtLeastTwo] (ho : Odd n) (hnp : ¬n.Prime) :
Fintype.card {a // SPP n a} * 4 ≤ n - 1
Miller–Rabin
/-- The *Miller–Rabin* primality test on input `n`, run `r` times. -/
def millerRabin {gen : Type*} [RandomGen gen] (g : gen) (n r : ℕ) :
Bool × gen
def runMillerRabin (n r : ℕ) : IO Bool
Possible extensions
- Show
millerRabinhas probability of correctness aribitrarily close to1whenrlarge enough and the random generatorgis uniform and independent enough - Verify Pratt, ECPP, Pocklington certificates (useful for proofs actually needing a particular large prime)
- More primality tests: Euler/Euler–Jacobi, (strong) Lucas, Baillie–PSW, AKS
- Format, docstrings, simplify / abstract lemmas from some long proofs