Erdős problem 400
Erdős and Graham write that it is easy to show that always, but the best possible constant is unknown.
Sources
FormalConjectures/ErdosProblems/
400.lean
Retained formal statement
For , . We show this by choosing .
∀ (k n : ℕ), k ≥ 2 → 0 < Erdos400.g k nTestStatement only, no proof