Erdős problem 241
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
241.lean
Retained formal statement
The best upper bound known to date is due to Green [Gr01], . (note that ).
∃ ε, (ε =o[Filter.atTop] fun x => 1) ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos241.f N 3) ≤ ((7 / 2) ^ (1 / 3) + ε N) * ↑N ^ (1 / 3)SolvedStatement only, no proof