Erdős problem 241

Is it true that $f(N)\sim N^{1/3}$ ?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

241.lean

Retained formal statement5 of 5

The best upper bound known to date is due to Green [Gr01], $f(N) \leq ((7/2)^{1/3}+o(1))N^{1/3}$ . (note that $(7/2)^{1/3}\approx 1.519$ ).

FormalConjectures/ErdosProblems/241.leanErdos241.erdos_241.variants.upper_bound3 linesExact file

1∃ ε,2  (ε =o[Filter.atTop] fun x => 1) ∧3    ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos241.f N 3) ≤ ((7 / 2) ^ (1 / 3) + ε N) * ↑N ^ (1 / 3)

SolvedStatement only, no proof