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

There exists $n$ such that Erdos961Prop k n holds.

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

1∀ (k : ℕ), 0 < k → ∃ n, Erdos961.Erdos961Prop k n

SolvedStatement only, no proof