proving a specific p is Prime

Stream: lean4

[David Stainton 🦡]

Lately I've been using mathlib's ZMod to make the prime order fields for various elliptic curves for cryptography such as X25519. However I've had to apologize to the Lean compiler for not being able to prove p is prime. Is there a known solution in Lean for proving a specific large p is prime? Looks like in the coq world there is coqprime which produces Pocklington certificates.

def p : ℕ := 2^255 - 19
def basepoint : ZMod p := 9
def keySize : ℕ := 32

theorem p_is_prime : Nat.Prime p := by sorry
instance fact_p_is_prime : Fact (Nat.Prime p) := ⟨p_is_prime⟩
instance : Field (ZMod p) := ZMod.instField p

[Ruben Van de Velde]

In theory this is a job for norm_num, but I don't know how well it handles big numbers

[Daniel Weber]

See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Practical.20ways.20to.20prove.20Nat.2EPrime.20N

[Daniel Weber]

This uses Pollard's rho algorithm for factoring p-1, which is too slow — you should probably manually create a Pratt certificate for your prime

[David Stainton 🦡]

Alright thanks! I'll look into creating a pratt certificate.