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 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