Erdős problem 975
For an irreducible polynomial with for sufficiently large , does there exists a constant such that ?
Sources
FormalConjectures/ErdosProblems/
975.lean
Retained formal statement
The correctness of the growth rate is shown in [Va39] (lower bound) and [Er52b] (upper bound).
∀ (f : Polynomial ℤ), Irreducible f → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → Erdos975.Erdos975Sum f =O[Filter.atTop] fun x => x * Real.log xSolvedStatement only, no proof