Erdős problem 961

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

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

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