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 for some .
∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (1 + c / Real.log (Real.log ↑n)) < ↑(Erdos1085.f 2 n)SolvedStatement only, no proof