Erdős Problem 1107

References:

• erdosproblems.com/1107
• [He88] Heath-Brown, D. R., Ternary quadratic forms and sums of three square-full numbers. (1988)

def Erdos1107.SumOfRPowerful (r n : ℕ) : Prop

Helper Property: $n$ is the sum of at most $r+1$ numbers, each of which is $r$-full.

Equations

• Erdos1107.SumOfRPowerful r n = ∃ (s : List ℕ), s.length ≤ r + 1 ∧ (∀ x ∈ s, r.Full x) ∧ s.sum = n

theorem Erdos1107.erdos_1107 (r : ℕ) : r ≥ 2 → ∀ᶠ (n : ℕ) in Filter.atTop, SumOfRPowerful r n

Let $r \ge 2$. Is every large integer the sum of at most $r + 1$ many $r$-powerful numbers?

theorem Erdos1107.erdos_1107.variants.two : ∀ᶠ (n : ℕ) in Filter.atTop, SumOfRPowerful 2 n

Heath-Brown [He88] proved every large integer the sum of at most three $2$-powerful numbers.