Practical ways to prove Nat.Prime N

Stream: maths

[Clarence Chew]

I'm thinking about finding practical ways to get Nat.Prime N (for N a given prime number) from a relatively small certificate of primality, and I'm not sure what the current state of the art is.

I'm looking into trying to generate Nat.Prime N from a factorization of N-1 and primitive root, but just going to ask to see if anyone has other more practical (smaller certificates/more efficient verification) ideas.

Other methods I have checked:
norm_num doesn't seem to work well for 3-digit primes, but I coded the following simple proof which basically does trial division up to the square root, which seems to work up to 4-digit primes.

example : Nat.Prime 101 := by
  rw [Nat.Prime]
  apply irreducible_iff.mpr
  norm_num
  intro a b hp
  wlog ha : a ≤ b generalizing a b with h
  exact if hb : b = 1 then Or.inr hb else Or.inl (Or.resolve_left (h b a ((mul_comm a b).subst (motive := fun x ↦ _ = x) hp) (Nat.le_of_not_le ha)) hb)
  have : a ≤ 10 := by
    by_contra! hla
    linarith [Nat.mul_le_mul hla (le_trans hla ha), hp]
  interval_cases a
  linarith [hp]
  exact Or.inl rfl
  repeat
    have := Dvd.intro b hp.symm
    norm_num at this

[Riccardo Brasca]

import Mathlib

example : Nat.Prime 101 := by norm_num

just works.

[Riccardo Brasca]

Ah sorry, you want a better proof?

[Riccardo Brasca]

import Mathlib

example : Nat.Prime 408643 := by norm_num

still works on my computer

[Markus Himmel]

I have a working but unpolished implementation of automatic generation and verification of pratt certificates here: https://github.com/leanprover-community/mathlib4/blob/6439ce3f194a2acd309af6831d753e560c46bcf6/Mathlib/NumberTheory/LucasPrimality.lean#L567

[Clarence Chew]

Strange, oh well, guess I didn't do my testing properly. The limit on my computer seems to be between 6 and 7 digits.

[Clarence Chew]

That aside, thanks for the reference to Pratt certificates.