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
Asymptotics for Erdos975Sum with .
∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum (Polynomial.X ^ 2 + 1) x / (x * Real.log x)) Filter.atTop (nhds c)SolvedStatement only, no proof