Erdős Problem 940

Reference: erdosproblems.com/940

theorem erdos_940 : (∀ r ≥ 3, {n : ℕ | ∃ (S : Multiset ℕ), S.card ≤ r ∧ (∀ s ∈ S, r.Full s) ∧ n = S.sum}.HasDensity 0) ↔ sorry

Let $r \ge 3$. Is it true that the set of integers which are the sum of at most $r$ $r$-powerful numbers has density $0$?

theorem erdos_940.variants.two : {n : ℕ | ∃ (S : Multiset ℕ), S.card ≤ 2 ∧ (∀ s ∈ S, Nat.Full 2 s) ∧ n = S.sum}.HasDensity 0

The set of integers which are the sum of at most two $2$-powerful numbers has density $0$.

theorem erdos_940.variants.three_cubes : {n : ℕ | ∃ (S : Multiset ℕ), S.card ≤ 3 ∧ n = (Multiset.map (fun (x : ℕ) => x ^ 3) S).sum}.HasDensity 0 ↔ sorry

Is it true that the set of integers which are the sum of at most three cubes has density $0$?

theorem erdos_940.variants.large_integers : (∀ r ≥ 2, ∀ᶠ (x : ℕ) in Filter.atTop, ∃ (S : Multiset ℕ), S.card ≤ r ∧ (∀ s ∈ S, r.Full s) ∧ x = S.sum) ↔ sorry

It is not known if all large integers are the sum of at most $r$-many $r$-powerful numbers.

theorem erdos_940.variants.three_powerful : ∀ᶠ (x : ℕ) in Filter.atTop, ∃ (S : Multiset ℕ), S.card ≤ 3 ∧ (∀ s ∈ S, Nat.Full 2 s) ∧ x = S.sum

Heath-Brown [He88] has proved that all large numbers are the sum of at most three $2$-powerful numbers.

[He88] Heath-Brown, D. R., Ternary quadratic forms and sums of three square-full numbers. (1988), 137--163.