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
For an irreducible polynomial with for sufficiently large , does there exists a constant such that ?
Note that it is unclear whether the polynomial should have integer coefficients or merely be integer-valued. We assume the former.
True ↔ ∀ (f : Polynomial ℤ), f.natDegree ≠ 0 → Irreducible f → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → ∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)OpenStatement only, no proof