Erdős problem 1085
Erdős and Pach showed that, for odd, there exist constants such that where .
Sources
FormalConjectures/ErdosProblems/
1085.lean
Retained formal statement
Erdős showed .
(fun n => ↑n ^ (4 / 3) * Real.log (Real.log ↑n)) =O[Filter.atTop] fun n => ↑(Erdos1085.f 3 n)SolvedStatement only, no proof