39.11.1. Introduction🔗

HexIntFactor factors natural numbers into primes. Every factorization it returns carries a primality certificate for each of its primes, and has been checked, so it can be used in proofs as well as in programs. From a factorization the library computes divisors, the divisor sums σ_k, Euler's totient, the radical, the decomposition into a squarefree part times a square, and the Carmichael function, and it certifies multiplicative orders and primitive roots.

Fermat conjectured that every number F_k = 2^(2^k) + 1 is prime. Euler found in 1732 that 641 divides F_5 = 2^32 + 1. The function Hex.Nat.factor? finds this factorization:

[641, 6700417]

Written out as data, the same factorization proves Euler's result as a statement about Mathlib's Nat.primeFactorsList. Nobody writes this data by hand: the command #int_factor, described in Factors found elsewhere, prints it.

The definition of eulerF5 lists the primes with their exponents and a certificate for each prime, and decide +kernel has Lean's kernel check them. The theorem Hex.Nat.CheckedFactorization.primeFactorsList_eq then identifies the checked list with Mathlib's. Nothing about how the factors were found enters the proof. The next section explains the certificate.

HexIntFactor does not depend on Mathlib. Import it to compute, and import HexIntFactorTheory for the theorems that translate its results into statements about Nat.factorization, Nat.primeFactorsList, Nat.divisors, Nat.totient and orderOf in ZMod n.

39.11.2. Factorizations and their certificates🔗

A Hex.Nat.Factorization is a number, its subject, and a list of entries of type Hex.Nat.PrimePower. An entry is an exponent and a primality certificate from HexPrimality; the prime of the entry, Hex.Nat.PrimePower.prime, is by definition the number the certificate is about, so an entry cannot name one prime and certify another.

In eulerF5 the entry ⟨1, .small 641⟩ is the prime 641 to the first power. Its certificate .small 641 says that 641 appears in HexPrimality's table of the primes below 10^5. The second entry is 6700417 to the first power, with a Pocklington certificate: 6700416 = 2^7 · 3 · 17449, and each triple gives a witness, the exponent of a prime factor of 6700416 minus one, and a certificate for that prime factor. The HexPrimality chapter describes these certificates and how they are checked.

Hex.Nat.checkFactorization accepts a factorization when the subject is positive, the primes are strictly increasing, every exponent is positive, every certificate is accepted by HexPrimality's checkPrime, and the product of the prime powers is the subject. It computes that product against the subject as a bound and stops as soon as the partial product exceeds it, so a factorization with an absurd exponent is rejected without computing an enormous power. A value of type CheckedFactorization n (Hex.Nat.CheckedFactorization) is a factorization together with proofs that its subject is n and that the checker accepts it. The arithmetic functions of this chapter take one. The number 1 has the empty factorization. To factor an integer, factor its absolute value.

Acceptance means more than that the product is right. If a prime q divides the product of the listed prime powers, it divides one of the listed primes, so it is one of them. The listed primes are therefore all the prime divisors of the subject, and each exponent is the exact power dividing it:

Hex.Nat.checkFactorization_primeSupport {F : Hex.Nat.Factorization}
  (h : Hex.Nat.checkFactorization F = true) {q : ℕ}
  (hq : Hex.Nat.Prime q) : q ∣ F.subject ↔ ∃ e ∈ F.factors, e.prime = q
Hex.Nat.checkFactorization_primeSupport
  {F : Hex.Nat.Factorization}
  (h :
    Hex.Nat.checkFactorization F = true)
  {q : ℕ} (hq : Hex.Nat.Prime q) :
  q ∣ F.subject ↔
    ∃ e ∈ F.factors, e.prime = q

Hex.Nat.checkFactorization_multiplicity {F : Hex.Nat.Factorization}
  (h : Hex.Nat.checkFactorization F = true) {e : Hex.Nat.PrimePower}
  (he : e ∈ F.factors) {k : ℕ} :
  e.prime ^ k ∣ F.subject ↔ k ≤ e.exponent
Hex.Nat.checkFactorization_multiplicity
  {F : Hex.Nat.Factorization}
  (h :
    Hex.Nat.checkFactorization F = true)
  {e : Hex.Nat.PrimePower}
  (he : e ∈ F.factors) {k : ℕ} :
  e.prime ^ k ∣ F.subject ↔ k ≤ e.exponent

Both the product identity and the primality of each listed factor are needed. 12 = 4 · 3 has the right product with a composite factor, and [3] lists only primes but misses one.

39.11.3. Finding factorizations🔗

Hex.Nat.factor? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ := Hex.Nat.defaultFuel n) (pMinusOneStage2 : Bool := false)
  (squfof : Hex.Nat.Squfof.Policy := Hex.Nat.Squfof.Policy.off) :
  Except Hex.Nat.FactorFailure
    (Hex.Nat.CheckedFactorization n × Hex.Rand)
Hex.Nat.factor? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ := Hex.Nat.defaultFuel n)
  (pMinusOneStage2 : Bool := false)
  (squfof : Hex.Nat.Squfof.Policy :=
    Hex.Nat.Squfof.Policy.off) :
  Except Hex.Nat.FactorFailure
    (Hex.Nat.CheckedFactorization n ×
      Hex.Rand)

The search is randomized. The caller supplies the random state, a Hex.Rand from HexBasic, and receives the advanced state with the result, so a computation is reproducible from its seed. The fuel argument bounds the number of cofactors the search processes and the work it spends on each; its default, Hex.Nat.defaultFuel, is 4 · ⌊log₂ n⌋ + 32. Each method also has fixed limits of its own, which more fuel does not raise.

To display results, this chapter uses a small helper that lists the primes of a factorization with their exponents. The numbers 2^(2^k) - 1 are products of Fermat numbers, 2^128 - 1 = F_0 · F_1 · ⋯ · F_6, and factor? finds all nine prime factors:

Except.ok [(3, 1), (5, 1), (17, 1), (257, 1), (641, 1), (65537, 1), (274177, 1), (6700417, 1), (67280421310721, 1)]

factor? first removes the powers of two and divides by the primes in HexPrimality's table, the primes below 10^5, and recognizes perfect powers. For each cofactor that remains, HexPrimality's certificate search tries to prove it prime, factoring p - 1 in turn. It may succeed, find a Miller–Rabin witness that the cofactor is composite, or run out of budget. If no certificate is found, the cofactor is split by Pollard's rho method with Brent's cycle detection, then by Pollard's p - 1 method and the elliptic curve method (ECM), and both pieces are processed again. The search is not trusted: the result is accepted only when the checker of the previous section accepts it. The work is in finding a factor. Rho is expected to find a prime factor p after about √p steps. Pollard's p - 1 method and ECM can find much larger factors when p - 1, or the order of a random elliptic curve modulo p, is a product of small primes, and the default bounds on those primes are small.

Except.ok ([3, 5, 17, 257, 641, 65537, 274177, 6700417], 22894341011050090868949881974522315437050433829130497)

Hex.Nat.checkPartial_prod {F : Hex.Nat.PartialFactorization}
  (h : Hex.Nat.checkPartial F = true) :
  (List.map (fun e => e.prime ^ e.exponent) F.factors).prod *
      F.residual =
    F.subject
Hex.Nat.checkPartial_prod
  {F : Hex.Nat.PartialFactorization}
  (h : Hex.Nat.checkPartial F = true) :
  (List.map
          (fun e => e.prime ^ e.exponent)
          F.factors).prod *
      F.residual =
    F.subject

Hex.Nat.checkFactorization_of_checkPartial
  {F : Hex.Nat.PartialFactorization} (h : Hex.Nat.checkPartial F = true)
  (hr : F.residual = 1) :
  Hex.Nat.checkFactorization
      { subject := F.subject, factors := F.factors } =
    true
Hex.Nat.checkFactorization_of_checkPartial
  {F : Hex.Nat.PartialFactorization}
  (h : Hex.Nat.checkPartial F = true)
  (hr : F.residual = 1) :
  Hex.Nat.checkFactorization
      { subject := F.subject,
        factors := F.factors } =
    true

Except.ok ([(184185251, 1), (218526229, 1)], 40249307935737000)

Hex.Nat.interleavedFactorSearch (trace : Bool := false)
  (early : Bool := true) : Hex.Nat.FactorSearch
Hex.Nat.interleavedFactorSearch
  (trace : Bool := false)
  (early : Bool := true) :
  Hex.Nat.FactorSearch

Hex.Nat.interleavedConstructionFactor : Hex.Nat.FactorSearch
Hex.Nat.interleavedConstructionFactor :
  Hex.Nat.FactorSearch

Hex.Nat.ecmFactorSearch (b₁ : ℕ := 32768) (b₂ : ℕ := 524288)
  (curves : ℕ := 64) (trace : Bool := false) : Hex.Nat.FactorSearch
Hex.Nat.ecmFactorSearch (b₁ : ℕ := 32768)
  (b₂ : ℕ := 524288) (curves : ℕ := 64)
  (trace : Bool := false) :
  Hex.Nat.FactorSearch

39.11.4. Arithmetic from a factorization🔗

Once a number is factored, its arithmetic functions are given by the usual formulas in the primes and exponents, and none of them searches. Euler proved in 1772 that 2^31 - 1 is prime, so that 2^30 · (2^31 - 1) is a perfect number: the sum of its divisors, σ_1, is twice the number.

Except.ok ([(2, 30), (2147483647, 1)], 62, true, 1152921503533105152)

Hex.Nat.numDivisors is the number of divisors, ∏ (eᵢ + 1); Hex.Nat.sigma F k is the sum of the kth powers of the divisors; Hex.Nat.totient is Euler's φ; and Hex.Nat.radical is the product of the distinct primes. These are evaluated from the prime powers, one term per prime. Hex.Nat.divisors generates all the divisors and sorts them into increasing order, so for D divisors it takes O(D log D) comparisons.

Hex.Nat.squareDivisor is the largest d such that d^2 divides n, and Hex.Nat.squarefreePart is n / d^2; they come from halving the exponents and from their parities. For the perfect number above they are 2^15 and 2^31 - 1.

Hex.Nat.squarefreePart_mul_square {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squarefreePart F * Hex.Nat.squareDivisor F ^ 2 = n
Hex.Nat.squarefreePart_mul_square {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squarefreePart F *
      Hex.Nat.squareDivisor F ^ 2 =
    n

Hex.Nat.squareDivisor_spec {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squareDivisor F ^ 2 ∣ n ∧
    ∀ (d : ℕ), d ^ 2 ∣ n → d ∣ Hex.Nat.squareDivisor F
Hex.Nat.squareDivisor_spec {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squareDivisor F ^ 2 ∣ n ∧
    ∀ (d : ℕ),
      d ^ 2 ∣ n →
        d ∣ Hex.Nat.squareDivisor F

39.11.5. Orders and primitive roots🔗

For n > 1 and a prime to n, the order of a modulo n is the least m > 0 with a^m ≡ 1 (mod n). Knowing a candidate m is not enough to check it, since a proper divisor of m might work too. With the factorization of m it suffices to check that a^m ≡ 1 and that a^(m/q) ≢ 1 for each prime q dividing m. An Hex.Nat.OrderCert records a, n, m and a factorization of m, and Hex.Nat.checkOrder makes these checks.

The "minimal standard" random number generator of Park and Miller multiplies by 16807 = 7^5 modulo the prime 2^31 - 1. From any nonzero seed it returns to its starting value only after 2^31 - 2 steps, because 16807 has order 2^31 - 2, that is, it is a primitive root. Every prime factor of 2^31 - 2 = 2 · 3^2 · 7 · 11 · 31 · 151 · 331 is in the table, so the certificate is short:

Hex.Nat.order_eq_of_checkOrder {c : Hex.Nat.OrderCert}
  (h : Hex.Nat.checkOrder c = true) :
  Hex.Nat.orderOf c.base c.modulus = c.order
Hex.Nat.order_eq_of_checkOrder
  {c : Hex.Nat.OrderCert}
  (h : Hex.Nat.checkOrder c = true) :
  Hex.Nat.orderOf c.base c.modulus =
    c.order

For a prime p, Hex.Nat.isPrimitiveRoot tests whether g has order p - 1, given a certificate that p is prime and a factorization of p - 1, and Hex.Nat.primitiveRoot? tries 2, 3, 4, … in turn and returns the first primitive root with its order certificate. Its last argument bounds the number of candidates, and it returns none when they run out. The least primitive root modulo 2^31 - 1 is 7:

some 7

Hex.Nat.carmichael computes the Carmichael function λ(n), the exponent of the group of units modulo n, as the least common multiple of its values on the prime powers. Every unit raised to λ(n) is 1 (Hex.Nat.pow_carmichael), and the order of every unit divides λ(n) (Hex.Nat.orderOf_dvd_carmichael). For 561 = 3 · 11 · 17, λ(561) = lcm(2, 10, 16) = 80, which divides 560. So a^560 ≡ 1 (mod 561) for every a prime to 561, although 561 is composite: it is the smallest Carmichael number.

Except.ok (#[1, 3, 11, 17, 33, 51, 187, 561], 80)

39.11.6. The Mathlib correspondence🔗

HexIntFactorTheory states the results of HexIntFactor in Mathlib's terms. It does no searching or checking of its own: each theorem takes a Hex.Nat.CheckedFactorization or an accepted Hex.Nat.OrderCert and identifies the values computed from it with Mathlib's definitions. With eulerF5 from the introduction and minstd from the previous section:

The first rewrites Mathlib's totient as the one computed from the factorization, which the kernel evaluates. The second identifies the order of 16807 in ZMod 2147483647 with Hex.Nat.orderOf, which the order certificate determines.

The basic statement is that the exponents of a checked factorization are Mathlib's Nat.factorization:

Hex.Nat.CheckedFactorization.factorization_eq {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) (p : ℕ) :
  n.factorization p =
    (List.find? (fun e => e.prime == p) F.raw.factors).elim 0 fun x =>
      x.exponent
Hex.Nat.CheckedFactorization.factorization_eq
  {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n)
  (p : ℕ) :
  n.factorization p =
    (List.find? (fun e => e.prime == p)
          F.raw.factors).elim
      0 fun x => x.exponent

The others have the same shape: Hex.Nat.CheckedFactorization.primeFactorsList_eq for Nat.primeFactorsList, Hex.Nat.divisors_eq for Nat.divisors, Hex.Nat.totient_eq for Nat.totient, Hex.Nat.sigma_eq for the sums of powers of divisors, Hex.Nat.isSquarefree_iff_squarefree for Squarefree, and Hex.Nat.orderOf_natCast and Hex.Nat.orderOf_eq for orderOf in ZMod n and its group of units.

39.11.7. Factors found elsewhere🔗

Finding a factor is the hard part of factoring, and checking one is easy. So a factor found by other software, or taken from the literature, can be supplied to Hex.Nat.importFactors, which certifies it. Morrison and Brillhart factored F_7 in 1970 with the continued fraction method. The search of When the search stops cannot find their factors, but given them, importFactors proves both prime in about a millisecond:

some [(59649589127497217, 1), (5704689200685129054721, 1)]

A proposal lists candidate factors with positive exponents, and optionally with primality certificates, in any order and with repetitions. Their product must divide the subject, and supplied certificates must be valid; otherwise importFactors returns an error. It searches for a certificate for each factor that lacks one. Factors it cannot certify, and whatever the proposal leaves unlisted, remain in the residual of a partial factorization; the result is complete exactly when that residual is 1. The first argument bounds the work and the size of the input; by default the subject has at most 256 bits.

The commands #int_factor and #int_factor_export, from HexIntFactor.Export, turn a factorization into Lean source. They run the program gp of PARI/GP to find the factors, when it is installed, and certify them as above; without PARI/GP, or for what PARI/GP leaves unfactored, they fall back on a short search of their own. In a module that imports HexIntFactor.Export,

#int_factor for 2 ^ 32 + 1

prints a module defining the factorization of 2^32 + 1 and its checked form, like eulerF5 in the introduction, and

#int_factor_export MyFactors.F5 cert for 2 ^ 32 + 1

writes that module to the new file MyFactors/F5.lean, refusing to overwrite an existing file. Other modules then import MyFactors.F5 and use MyFactors.F5.cert_checked. The generated module imports only HexIntFactor.Replay, which contains the checker and none of the search, so it builds without PARI/GP. The commands run only in a batch build, such as lake build +MyModule, and not in the editor; remove the command once its output has been saved. They accept subjects of at most 256 bits.

39.11.8. Very large prime factors🔗

A Pocklington certificate for a prime p requires a sufficiently large factored divisor of p - 1. When that is hard to find, elliptic curve primality proofs (HexECPP) offer another way. The module HexIntFactor.Mixed.Replay defines factorizations, Hex.Nat.Mixed.Factorization, in which each prime carries either a HexPrimality certificate or an elliptic curve certificate, and HexIntFactor.Mixed.Import imports them, trying elliptic curve certificates for primes of up to 256 or 512 bits when asked to. The commands #int_factor_mixed and #int_factor_mixed_export of HexIntFactor.Mixed.Export produce such factorizations as source, from supplied factors or from PARI/GP.

HexIntFactorTheory.Mixed provides the same correspondence with Nat.factorization for these factorizations:

Hex.Nat.Mixed.CheckedFactorization.factorization_eq {n : ℕ}
  (F : Hex.Nat.Mixed.CheckedFactorization n) (p : ℕ) :
  n.factorization p =
    (List.find? (fun e => e.prime == p) F.raw.factors).elim 0 fun x =>
      x.exponent
Hex.Nat.Mixed.CheckedFactorization.factorization_eq
  {n : ℕ}
  (F :
    Hex.Nat.Mixed.CheckedFactorization n)
  (p : ℕ) :
  n.factorization p =
    (List.find? (fun e => e.prime == p)
          F.raw.factors).elim
      0 fun x => x.exponent

The arithmetic functions of this chapter take the ordinary Hex.Nat.CheckedFactorization. Hex.Nat.Mixed.CheckedFactorization.ofLegacy converts an ordinary factorization to the mixed form, and Hex.Nat.Mixed.CheckedFactorization.toLegacy converts back when every prime carries a HexPrimality certificate.

39.11.9. Costs and limits🔗

Checking a factorization checks each primality certificate and rebuilds the product with arithmetic bounded by the subject. Checking an order certificate also computes a^m mod n, and a^(m/q) mod n for each prime q dividing m. Both are cheap next to finding the factorization.

Splitting a number is usually the expensive part: rho is expected to find a prime factor p in about √p steps, so the size of the second largest prime factor matters most, since the largest is left over as the final cofactor. Each prime found must then be certified, which needs a partial factorization of p - 1 and can be expensive in turn. Whether a search succeeds therefore depends on the factors, on p - 1 for each of them, on the seed and on the fuel. When the search fails, supply the factors as in Factors found elsewhere.

These times were measured on one core of a shared machine (chungus2) on 2026-10-05, one run each, by evaluating the functions in a compiled module:

39.11.10. Cross-references🔗

• HexPrimality provides the primality certificates, the table of small primes, Pollard's rho and p - 1 methods, and the multiplicative order Hex.Nat.orderOf.

• HexECPP provides the elliptic curve primality certificates used by the mixed factorizations.

• HexBasic provides the random state Hex.Rand.