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.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

1094.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/1094.leanErdos1094.erdos_10941 lineExact file

1{(n, k) | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite

OpenStatement only, no proof