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 statement1 of 6

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

FormalConjectures/ErdosProblems/961.leanErdos961.erdos_9611 lineExact file

1True ↔ ∃ C, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos961.f k) < Real.log ↑k ^ C

OpenStatement only, no proof