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
Is the lower bound in 3D also an upper bound?.
True ↔ (fun n => ↑(Erdos1085.f 3 n)) =O[Filter.atTop] fun n => ↑n ^ (4 / 3) * Real.log (Real.log ↑n)OpenStatement only, no proof