Erdős problem 1107
Let . Is every large integer the sum of at most many -powerful numbers?
Sources
FormalConjectures/ErdosProblems/
1107.lean
Retained formal statement
Heath-Brown [He88] proved every large integer the sum of at most three -powerful numbers.
∀ᶠ (n : ℕ) in Filter.atTop, Erdos1107.SumOfRPowerful 2 nSolvedStatement only, no proof