Prove2Me

GNFS: base-mm polynomial and homogenization

Definition
GNFS_defs

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

integer-factorizationnumber-theory

Two auxiliary objects used throughout the mission.

  1. Base-mm polynomial. For natural numbers nn and mm, let n=admd+⋯+a1m+a0n = a_d m^d + \dots + a_1 m + a_0 be the base-mm expansion of nn, with digits a0,…,ada_0, \dots, a_d (least significant first, as returned by the standard digit expansion; empty when n=0n = 0). The base-mm polynomial of nn is
fn,m(x)=∑i=0daixi∈Z[x].f_{n,m}(x) = \sum_{i=0}^{d} a_i x^i \in \mathbb{Z}[x].
  1. Homogenization. For f=∑i=0dcixi∈Z[x]f = \sum_{i=0}^{d} c_i x^i \in \mathbb{Z}[x] of degree dd and integers a,ba, b,
F(a,b)=∑i=0dci aibd−i=bdf(a/b).F(a,b) = \sum_{i=0}^{d} c_i\, a^i b^{d-i} = b^d f(a/b).

The first is the simple polynomial-selection method of GNFS; the second is the integer rr attached to a relation (a,b)(a,b), whose smoothness the sieve tests.

Formalization Note Digits come from Nat.digits m n. For m≤1m \le 1 that function does not give a base-mm expansion, so statements about it assume m≥2m \ge 2. In homogenize, 00=10^0 = 1, so F(a,0)=cdadF(a,0) = c_d a^d.

Definition code
import Mathlib

/-!
# General number field sieve — definitions

Shared definitions for the Prove2Me mission proposal drafted from the Wikipedia article
"General number field sieve" (`General_number_field_sieve.pdf`).
-/

open Polynomial

namespace GNFS

/-- The base-`m` polynomial of `n`: if `n = a_d m^d + ⋯ + a_1 m + a_0` is the base-`m`
expansion of `n` (digits `0 ≤ a_i < m`), this is `f(x) = a_d x^d + ⋯ + a_1 x + a_0`. -/
noncomputable def baseMPolynomial (n m : ℕ) : ℤ[X] :=
  ∑ i ∈ Finset.range (Nat.digits m n).length, C (((Nat.digits m n).getD i 0 : ℕ) : ℤ) * X ^ i

/-- The homogenization `F(a, b) = b^d f(a/b) = ∑ c_i a^i b^(d-i)` of an integer polynomial
`f = ∑ c_i x^i` of degree `d`, evaluated at a pair of integers `(a, b)`. -/
def homogenize (f : ℤ[X]) (a b : ℤ) : ℤ :=
  ∑ i ∈ Finset.range (f.natDegree + 1), f.coeff i * a ^ i * b ^ (f.natDegree - i)

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), sections 'Polynomial choice' and 'Generation of relation pairs (sieving)'
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