Formal target: Corpus.Erdos1093.erdos_1093.parts.ii

Are there only finitely many binomial coefficients with deficiency > 1?

Exact formal statement

Set.Finite.{0}
  (Set.ofPred.{0} fun x =>
    have k := Prod.fst.{0, 0} x;
    have n := Prod.snd.{0, 0} x;
    And (LE.le.{0} (HMul.hMul.{0, 0, 0} 2 k) n)
      (And (GT.gt.{0} (Corpus.Erdos1093.deficiency n k) 1)
        (∀ (p : Nat), Nat.Prime p → Dvd.dvd.{0} p (n.choose k) → LT.lt.{0} k p)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record