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 statement3 of 4

For $k \ge 2$ , $g_k(n) > 0$ . We show this by choosing $a = (n, 1, 0, \ldots, 0)$ .

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

1∀ (k n : ℕ), k ≥ 2 → 0 < Erdos400.g k n

TestStatement only, no proof