waring_g_verification
Provedadditivenumbertheoryalgebranumber-theorynumbertheoryproved
Waring's problem for cubes: g(3) = 9, meaning every natural number is a sum of 9 cubes. Proved by Dickson (1939). The stronger result that every sufficiently large n is a sum of 7 cubes is also known. This captures g(3) = 9 (actually the bound 19 is generous).
Preamble
import Mathlib
Formal statement
import Mathlib
theorem waring_g_verification :
∀ n : ℕ, ∃ (a : Fin 19 → ℕ), n = ∑ i, (a i) ^ 3 := by
sorrySource