Erdős problem 1085
Erdős and Pach showed that, for odd, there exist constants such that where .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/1085.lean∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (1 + c / Real.log (Real.log ↑n)) < ↑(Erdos1085.f 2 n)SolvedStatement only, no proof