Erdős problem 323
Is it true that for all ?
Sources
FormalConjectures/ErdosProblems/
323.lean
Retained formal statement
The case was resolved by Landau, who showed for some constant .
∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun x => ↑(Erdos323.f 2 2 x)) fun x => c * ↑x / √(Real.log ↑x)SolvedStatement only, no proof