waring_cubes_mod_p
Provedadditivenumbertheoryalgebramodulararithmeticnumber-theorynumbertheoryopen-problemopenproblem
Waring's problem mod p (for cubes): Every element of ℤ/pℤ is a sum of g cubes. For p ≡ 1 (mod 3), g = 5 is conjectured. Best known bounds involve character sum estimates. Exact g(3, p) for specific primes is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem waring_cubes_mod_p (p : ℕ) (hp : Nat.Prime p) (h3 : 3 ∣ p - 1) :
∃ (g : ℕ) (_ : g ≤ 5), ∀ n : ZMod p,
∃ (xs : Fin g → ZMod p), n = ∑ i, xs i ^ 3 := by
sorrySource