3.4. The Mathlib correspondence🔗

The two predicates agree, and the companion registers a handler on the same syntax kind, so the tactic closes Mathlib-stated goals directly:

example : Nat.Prime 2147483647 := by⊢ Nat.Prime 2147483647 primalityAll goals completed! 🐙

theorem

Hex.Nat.prime_iff {n : ℕ} : Hex.Nat.Prime n ↔ Nat.Prime n
Hex.Nat.prime_iff {n : ℕ} :
  Hex.Nat.Prime n ↔ Nat.Prime n

The whole correspondence: the Mathlib-free predicate and Nat.Prime agree. Everything else transports along it.

An ordinary import leaves Mathlib's Nat.Prime norm_num behavior unchanged: its trial-division extension registered before Hex's and is therefore consulted first. A module that wants the supported Hex policy opts in explicitly. Numerals below 2^24 then use a guarded trial-division alias, while 25-bit and larger numerals use bounded certificate search:

use_hex_primality_norm_num

example : Nat.Prime 2147483647 := by⊢ Nat.Prime 2147483647 norm_numAll goals completed! 🐙
example : ¬ Nat.Prime 2147483649 := by⊢ ¬Nat.Prime 2147483649 norm_numAll goals completed! 🐙
example : Nat.Prime 101 := by⊢ Nat.Prime 101 norm_numAll goals completed! 🐙

The choice is per-module and does not persist across imports. If bounded certificate or factor search exhausts above the threshold, the Hex policy fails rather than falling back to a large trial-division computation.