Miller–Rabin Primality Test in Lean
This repository formalizes the Miller–Rabin primality test in Lean. It contains both a runnable algorithm millerRabin and a proof that it returns true on a composite number with probability at most 1/4.
Main definitions
Fermat probable primality
/--
`n` is a *Fermat probable prime* to base `a` if `a ^ (n - 1) ≡ 1 (mod n)`.
-/
def FPP (n : ℕ) (a : ZMod n) : Prop :=
a ^ (n - 1) = 1
/-- This provides an algorithm for deciding `FPP`. -/
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
Strong probable primality, Miller–Rabin algorithm
/--
Let `n : ℕ` and let `n - 1 = 2 ^ s' * d` where `d` is odd.
`n` is a *strong probable prime* to base `a`, if `a ^ d = 1` or `∃ s < s', a ^ (2 ^ s * d) = -1`.
We also say `a` is a *nonwitness* to the primality of `n`.
-/
def SPP (n : ℕ) (a : ZMod n) : Prop :=
a ^ oddPart (n - 1) = 1 ∨
∃ s < val₂ (n - 1), a ^ (2 ^ s * oddPart (n - 1)) = -1
/-- The single-pass *Miller–Rabin algorithm* that decides `SPP` in $O(\log^3 n)$. -/
def SPP.millerRabin (n : ℕ) (a : ZMod n) : Bool
/-- `millerRabin` decides `SPP`. -/
lemma SPP.millerRabin_eq_true_iff {n : ℕ} (a : ZMod n) :
SPP.millerRabin n a = true ↔ 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 odd composite `n` in `ZMod n \ {0}` is at most 1/4.
-/
theorem SPP.card_le_of_not_prime {n : ℕ} [hn : Fact (1 < n)] (ho : Odd n) (hnp : ¬n.Prime) :
4 * #{a | SPP n a} ≤ n - 1
Next step
Better framework for probabilistic programs that are both provable and executable.