Primality certificates

The type of primality certificates and the certifier that constructs a Nat.Prime proof term.

inductive Mathlib.Tactic.Primality.Cert : Type

A primality certificate for p (not recorded in the type).

• normNum : Cert

  p is proved prime by norm_num.

• known : Cert

  A proof that p is prime is provided, which should be stored in the initial state of certifyPrime.

• lucas (root : ℕ) (factorization : List (ℕ × ℕ × Cert)) : Cert

  A Lucas certificate with the primitive root root and the factorization of p - 1 in factorization, each prime factor with its exponent and certificate.

partial def Mathlib.Tactic.Primality.certifyPrime (p : ℕ) (cert : Cert) : StateT (Std.HashMap ℕ Lean.Expr) Lean.MetaM Q(Nat.Prime «$p»)

Proves Nat.Prime p from the certificate cert. Each prime is proved only once.