Erdős problem 283
Let be a polynomial whose leading coefficient is positive and such that there exists no with for all . Is it true that, for all sufficiently large , there exist integers such that and ?
Sources
FormalConjectures/ErdosProblems/
283.lean
Retained formal statement
Cassels [Ca60] has proved that these conditions on the polynomial imply every sufficiently large integer is the sum of with distinct .
∀ (p : Polynomial ℤ), 0 < p.leadingCoeff → (¬∃ d ≥ 2, ∀ n ≥ 1, d ∣ Polynomial.eval n p) → ∀ᶠ (m : ℕ) in Filter.atTop, ∃ S, (∀ n ∈ S, 1 ≤ n) ∧ ∑ n ∈ S, Polynomial.eval (↑n) p = ↑mSolvedStatement only, no proof