Erdős problem 1094
For all the least prime factor of is , with only finitely many exceptions.
Sources
FormalConjectures/ErdosProblems/
1094.lean
Retained formal statement
For all the least prime factor of is , with only finitely many exceptions.
{(n, k) | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.FiniteOpenStatement only, no proof