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
Burr has proved this if with and if we allow .
∀ k ≥ 1, ∀ᶠ (m : ℕ) in Filter.atTop, ∃ M, (∀ n ∈ M, 1 ≤ n) ∧ (Multiset.map (fun n => 1 / n) do let a ← M pure ↑a).sum = 1 ∧ (Multiset.map (fun n => n ^ k) do let a ← M pure ↑a).sum = ↑mSolvedStatement only, no proof