Erdős problem 961 · problems.science

It is conjectured that $f(k) \ll (\log k)^O(1)$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

961.lean

Retained formal statement3 of 6

Erdos [Er55d] proved $f(k) < 3 \frac{k}{\log k}$ for sufficiently large $k$ .

FormalConjectures/ErdosProblems/961.leanErdos961.erdos_961.variants.erdos_upper_bound1 lineExact file

1∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos961.f k) < 3 * ↑k / Real.log ↑k

SolvedStatement only, no proof