Prove2Me

Base-mm polynomial: f(m)=nf(m)=n with digits 0≤ai<m0\le a_i<m

Proved
GNFS.baseMPolynomial_spec

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

integer-factorizationnumber-theory

Let n,mn, m be natural numbers with m≥2m \ge 2, and let fn,m(x)=∑iaixif_{n,m}(x) = \sum_i a_i x^i be the base-mm polynomial of nn, whose coefficients are the base-mm digits of nn. Then:

  1. fn,m(m)=nf_{n,m}(m) = n;
  2. every coefficient satisfies 0≤ai<m0 \le a_i < m (coefficients beyond the degree are 00);
  3. mm is a root of fn,mf_{n,m} modulo nn, i.e. fn,m(m)≡0(modn)f_{n,m}(m) \equiv 0 \pmod n.

This is the basic polynomial-selection step of GNFS, paired with g(x)=x−mg(x) = x - m.

Preamble
import Mathlib
import Definitions.Def_GNFS_defs
open Polynomial IntermediateField
Formal statement
namespace GNFS
theorem baseMPolynomial_spec (n m : ℕ) (hm : 2 ≤ m) :
    (baseMPolynomial n m).eval (m : ℤ) = n ∧
      (∀ i, 0 ≤ (baseMPolynomial n m).coeff i ∧ (baseMPolynomial n m).coeff i < m) ∧
      ((baseMPolynomial n m).map (Int.castRingHom (ZMod n))).IsRoot (m : ZMod n) := by sorry
end GNFS
Source
Wikipedia, "General number field sieve" (revision oldid=1377718368, https://en.wikipedia.org/w/index.php?title=General_number_field_sieve&oldid=1377718368), section 'Method — Polynomial choice'
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph