Wieferich's theorem g(3) = 9

wieferich_g_three — a formalization challenge from the lean-eval benchmark.

Notes

Every natural number is a sum of nine cubes, and nine is necessary (23 is not a sum of eight cubes): the k=3 case of the Hilbert–Waring problem, g(3) = 9. The trusted helper IsSumOfCubes (non-hole) fixes 'sum of k cubes'. Mathlib has Lagrange's four-square theorem but no Hilbert–Waring material (no g(k), no sum-of-cubes predicate, no g(3)=9). Candidate from §76 of the Knill survey.

Formal statement

/-- **Wieferich's theorem `g(3) = 9`.** Every natural number is a sum of nine
cubes, and nine is necessary: some `n` (namely `23`) is not a sum of eight
cubes. -/
theorem wieferich_g_three :
    (∀ n : ℕ, IsSumOfCubes 9 n) ∧ ∃ n : ℕ, ¬ IsSumOfCubes 8 n := by
  sorry

Informal solution sketch

Two parts. Upper bound (g(3) ≤ 9, every n is a sum of nine cubes): the classical Wieferich–Kempner argument — reduce to a bounded range via the identity expressing six consecutive integers' cubes and the fact that every sufficiently large n is a sum of at most eight cubes (Linnik/Watson give 8 for large n), then check the finite remaining range by computation, the worst cases being 23 and 239 (both of which need nine cubes). Lower bound (g(3) ≥ 9): exhibit n = 23, whose only cube summands ≤ 23 are 1 and 8; 23 = 2·8 + 7·1 uses nine cubes and a short case analysis shows no representation uses eight or fewer.

Source

A. Wieferich, Beweis des Satzes, daß sich eine jede ganze Zahl als Summe von höchstens neun positiven Kuben darstellen läßt, Math. Ann. 66 (1909); A. Kempner, Über das Waringsche Problem und einige Verallgemeinerungen, Math. Ann. 72 (1912). Knill, Some fundamental theorems in mathematics, §76.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: wieferich_g_three
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.