Erdős problem 387
Is there an absolute constant such that, for all , the binomial coefficient has a divisor in ?
Sources
FormalConjectures/ErdosProblems/
387.lean
Retained formal statement
It is easy to see that n.choose k has a divisor in [n / k, n].
∀ {n k : ℕ}, 1 ≤ n → k ≤ n → ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose kSolvedStatement only, no proof