Erdős problem 400

Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

400.lean

Retained formal statement4 of 4

Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

FormalConjectures/ErdosProblems/400.leanErdos400.erdos_400.variants.upper_bound1 lineExact file

1∀ k ≥ 2, (fun n => ↑(Erdos400.g k n)) =O[Filter.atTop] fun n => Real.log ↑n

SolvedStatement only, no proof