Erdős Problem 1094

For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions.

Reference: erdosproblems.com/1094

theorem Erdos1094.erdos_1094 : {(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite

Erdős problem 1094

There are only finitely many pairs (n,k) with n ≥ 2*k for which the least prime factor of the binomial coefficient Nat.choose n k exceeds max (n / k) k.