Formal target: Corpus.Erdos1094.erdos_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.

Exact formal statement

Set.Finite.{0}
  (Set.ofPred.{0} fun x =>
    Corpus.Erdos1094.erdos_1094.match_1.{1} (fun x => Prop) x fun n k =>
      And (LT.lt.{0} 0 k)
        (And (LE.le.{0} (HMul.hMul.{0, 0, 0} 2 k) n)
          (GT.gt.{0} (n.choose k).minFac (Max.max.{0} (HDiv.hDiv.{0, 0, 0} n k) k))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record