Erdős problem 683
There exists such that for all .}
Sources
FormalConjectures/ErdosProblems/
683.lean
Retained formal statement
Sylvester and Schur [Er34] proved that for .
∀ (n k : ℕ), 0 < k ∧ k ≤ n / 2 → Erdos683.P n k > kSolvedStatement only, no proof