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 statement3 of 5

Bose and Chowla [BoCh62] provided a construction proving one half of this, namely $(1+o(1))N^{1/3}\leq f(N)$ .

FormalConjectures/ErdosProblems/241.leanErdos241.erdos_241.variants.lower_bound1 lineExact file

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

SolvedStatement only, no proof