3.1. Introduction🔗

HexPrimality decides primality far past trial division and proves its positive answers in the kernel. The engine is the Pocklington certificate: an untrusted, randomized search factors n - 1, assembles a certificate, and the kernel replays a Boolean checker on that certificate by reduction alone. Nothing about the search — randomness, fuel, Pollard rho — appears in the proof term.

The library is Mathlib-free and states its results for the project-local Hex.Nat.Prime predicate. The companion library HexPrimalityMathlib transports everything to Mathlib's Nat.Prime, extends the primality tactic to goals stated with it, and registers an explicitly opted-in norm_num policy.