34.5.1. Start here🔗

Use a checkout of the hex-dev repository. The ECM provider is part of HexIntFactor, which is not yet included in the published split libraries. Start a Lean file with these imports:

The examples use Hex.Nat.Prime, so they need no Mathlib import. To state the same goals with Nat.Prime, also import HexPrimalityMathlib. The same tactic syntax then applies.

Put the examples in a section with local options:

The finite heartbeat allowance accommodates certificate construction. All three examples pass with this option alone; it is a tested allowance, not a measured minimum. It does not increase the factor search's shared 1024-attempt budget. Lean 4.34.0 may warn that the powers with exponents 384 and 448 exceed its shortcut threshold of 256. The goals still normalize and the proofs succeed; these examples leave that warning visible.

34.5.2. Three proofs🔗

The secp256k1 field prime is 2^256 - 2^32 - 977:

example : Hex.Nat.Prime (2 ^ 256 - 2 ^ 32 - 977) := by
  primality?

The P-384 field prime is 2^384 - 2^128 - 2^96 + 2^32 - 1:

example : Hex.Nat.Prime
    (2 ^ 384 - 2 ^ 128 - 2 ^ 96 + 2 ^ 32 - 1) := by
  primality?

The Curve448 field prime is 2^448 - 2^224 - 1:

example : Hex.Nat.Prime (2 ^ 448 - 2 ^ 224 - 1) := by
  primality?

Close the section after the examples:

Each proof produces a Try this: suggestion containing a complete certificate. Apply the suggestion to replace the search with a proof that replays that certificate. This is particularly useful when sharing a file: other people can check the proof without repeating the factor search.

The standard import makes bounded ECM available automatically. Construction first tries HexPrimality's own methods. If they exhaust with attempts left, it retries with ECM, carrying forward the random state and charging both routes to the same allowance. P-521 and Curve25519 finish on the first route. You do not need to supply factors, curve parameters, seeds or certificates. The expert override primality? (factor := Hex.Nat.ecmFactorSearch) selects that provider directly and bypasses automatic selection. To retain the core-only route, including its faster exhaustion on some unsupported inputs, use primality? (factor := Hex.Nat.Construction.factorSearch). Automatic retry can add substantial work even when it ultimately fails: the tested 507-bit fixture increased from about 0.9 seconds to 20.7 seconds.

If Lean reports a heartbeat limit, include the local option from the setup. A message saying that certificate construction exhausted its attempts instead refers to the factor search budget and identifies the unresolved subject. The factor-search reference describes the optional bounds, curve count and tracing arguments.

Build note: the three construction examples and their exact Try this: suggestions are checked in the field construction tests. Run lake build HexIntFactorFieldConformance to check them together. The manual build checks the saved proof below without repeating the searches.

34.5.3. What the saved proof looks like🔗

Here is a saved secp256k1 certificate in full, with abbreviated constructor names. This standalone proof needs only import HexPrimality.Cert and uses the numeral to avoid the options for normalizing powers:

The kernel checks the certificate through Hex.Nat.prime_of_checkPrimeAt. The search is untrusted: finding a factor is not enough to establish primality, and every necessary recursive certificate must pass the same checker. The complete saved certificates also include P-384 and Curve448.

34.5.4. How long does it take?🔗

Allow a few minutes to try all three searches in Lean. Construction and its factor provider run natively during elaboration; the complete module build also includes imports, certificate rendering and kernel checking.

The recorded shared-host automatic-construction medians were 26.0 seconds for secp256k1, 32.2 seconds for P-384, and 21.6 seconds for Curve448. Direct kernel replay medians were about 3.6–11.8 milliseconds per proof, excluding imports and elaboration. These are host-specific observations, not time limits or guarantees. See the automatic construction report for separate construction, rendering, kernel and caller-resource measurements, and the ECM construction report for the explicit-provider experiments.

The native search is synchronous. Lean can report a heartbeat overrun only after that computation returns; the heartbeat allowance is not a wall-clock timeout. The finite attempt limit bounds the search schedule.

The search has a fixed, bounded schedule and can still exhaust on other primes. The primality construction reference explains reusable certificates and the available budget override.