Fermat polygonal number theorem

3 fully proved

Gauss's Eureka theorem and Cauchy's lemma

TheoremGauss's Eureka theorem#✓fully proved

Every natural number \(n\) is a sum of three triangular numbers: there are natural numbers \(x, y, z\) with \(n = T_x + T_y + T_z\), where \(T_m = m(m + 1)/2\) is the \(m\)-th triangular (\(3\)-gonal) number, so that \(T_0 = 0\).

theorem exists_eq_add_add_triangular (n : ℕ) :
    ∃ x y z : ℕ, n = polygonalNumber 3 x + polygonalNumber 3 y + polygonalNumber 3 z

Sources

C. F. Gauss, Disquisitiones Arithmeticae (1801), as cited in Nathanson (1987), whose introduction gives the equivalent form used here: 8n + 3 is a sum of three odd squares.

Uses 3 · Used by 1

Statement usesPolygonal numbers

Proof usesLegendre's three-square theorem · Closed form of the triangular numbers

Used byFermat polygonal number theorem

TheoremCauchy's lemma#✓fully proved

Let \(a\) and \(b\) be odd natural numbers with \(b^2 < 4a\) and \(3a < b^2 + 2b + 4\). Then there are natural numbers \(s, t, u, v\) with \(a = s^2 + t^2 + u^2 + v^2\) and \(b = s + t + u + v\).

theorem exists_sum_four_sq_eq_and_sum_eq_of_odd {a b : ℕ}
    (ha : a % 2 = 1) (hb : b % 2 = 1) (hba : b ^ 2 < 4 * a)
    (hab : 3 * a < b ^ 2 + 2 * b + 4) :
    ∃ s t u v : ℕ, a = s ^ 2 + t ^ 2 + u ^ 2 + v ^ 2 ∧ b = s + t + u + v

Sources

M. B. Nathanson, A short proof of Cauchy's polygonal number theorem, Proc. Amer. Math. Soc. 99 (1987), 22-24, "Cauchy's Lemma"; originally Cauchy (1813-15).

Uses 1 · Used by 1

Proof usesLegendre's three-square theorem

Used byFermat polygonal number theorem

Fermat polygonal number theorem

TheoremFermat polygonal number theorem#✓fully proved

For every natural number \(s \ge 3\), every natural number \(n\) is a sum of at most \(s\) \(s\)-gonal numbers: there are a finite set \(T\) with at most \(s\) elements and natural numbers \(k_i\) for \(i \in T\) such that \(n = \sum_{i \in T} P_s(k_i)\), where \(P_s(m) = (s - 2)\binom{m}{2} + m\) is the \(m\)-th \(s\)-gonal number. The \(k_i\) may repeat, and since \(P_s(0) = 0\) the case \(n = 0\) is the empty sum.

The cases \(s = 3\) and \(s = 4\) follow from Gauss's three-triangular-number theorem and Lagrange's four-square theorem. For \(s \ge 5\), Cauchy's lemma and Nathanson's argument for \(n \ge 120(s - 2)\) (Nathanson 1987, Theorem 1) are combined with explicit families of representations for small \(n\) and a finite computation for the remaining cases.

theorem fermat_polygonal_number_theorem : ∀ (s n : ℕ), 3 ≤ s →
    ∃ (t : Finset ℕ) (k : ℕ → ℕ), t.card ≤ s ∧
      n = ∑ i ∈ t, Nat.polygonalNumber s (k i)

Sources

https://en.wikipedia.org/wiki/Fermat_polygonal_number_theorem.

Uses 5

Statement usesPolygonal numbers

Proof usesGauss's Eureka theorem · Cauchy's lemma · Square numbers as polygonal numbers · Polygonal numbers at one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.