Erdős problem 387

Is there an absolute constant $c > 0$ such that, for all $1 \leq k < n$ , the binomial coefficient $\binom{n}{k}$ has a divisor in $(cn, n]$ ?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

387.lean

Retained formal statement2 of 4

It is easy to see that n.choose k has a divisor in [n / k, n].

FormalConjectures/ErdosProblems/387.leanErdos387.erdos_387.variants.easy1 lineExact file

1∀ {n k : ℕ}, 1 ≤ n → k ≤ n → ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose k

SolvedStatement only, no proof