Waring's problem for cubes

DefinitionSum of \(k\) cubes#✓fully proved

A natural number \(n\) is a sum of \(k\) cubes if there are natural numbers \(x_1, \dots, x_k\) with \(n = x_1^3 + \dots + x_k^3\).

def IsSumOfCubes (k n : ℕ) : Prop :=
  ∃ x : Fin k → ℕ, ∑ i, (x i) ^ 3 = n

Used by 1

Used byWieferich's nine cubes theorem

TheoremWieferich's nine cubes theorem#●ready to prove

Every natural number is a sum of \(9\) cubes of natural numbers, and \(9\) cannot be replaced by \(8\): some natural number is not a sum of \(8\) cubes of natural numbers.

public theorem_wanted wieferich_g_three :
    (∀ n : ℕ, IsSumOfCubes 9 n) ∧ ∃ n : ℕ, ¬ IsSumOfCubes 8 n

Sources

• 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. Problem wieferich_g_three of the lean-eval benchmark.

Uses 1

Statement usesSum of \(k\) cubes

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.