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
Lower bound for the growth rate of Erdos975Sum, shown in [Va39].
∀ (f : Polynomial ℤ), Irreducible f → f.natDegree ≠ 0 → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → (fun x => x * Real.log x) =O[Filter.atTop] Erdos975.Erdos975Sum fSolvedStatement only, no proof