Congruence of squares gives a nontrivial factor

Proved

GNFS.nontrivial_gcd_of_sq_eq_sq

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

integer-factorizationnumber-theory

Let $n \in \mathbb{N}$ and $x, y \in \mathbb{Z}$ with

n \mid x^2 - y^2, \qquad n \nmid x - y, \qquad n \nmid x + y.

Then $\gcd(x - y, n)$ is a nontrivial divisor of $n$ :

1 < \gcd(x-y, n) < n.

This is the final step of every congruence-of-squares factoring method.

Preamble

import Mathlib
import Definitions.Def_GNFS_defs
open Polynomial IntermediateField

Formal statement

namespace GNFS
theorem nontrivial_gcd_of_sq_eq_sq (n : ℕ) (x y : ℤ) (h : (n : ℤ) ∣ x ^ 2 - y ^ 2)
    (hsub : ¬ (n : ℤ) ∣ x - y) (hadd : ¬ (n : ℤ) ∣ x + y) :
    1 < Int.gcd (x - y) n ∧ Int.gcd (x - y) n < 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 — Postprocessing'

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