Combinatorics

Erdős 1093 - part ii

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

References

erdosproblems.com/1093

No one has attempted this yet.

Formal statement

Lean type

{x |
    have k := x.1;
    have n := x.2;
    2 * k ≤ n ∧ Erdos1093.deficiency n k > 1 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ n.choose k → k < p}.Finite

What you must prove

import FormalConjectures.ErdosProblems.«1093»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1093.erdos_1093.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1093.lean

Source type SHA-256: sha256:0cdd45a79a7b1b196b24d1461cc697022e80f49b08b39b7a5677df26e6cc41c5
Task id: fc-379fc029-parts-ii-2ad1578658-formalized-v1
Task commitment: sha256:7dac230ac9b2ee1669fd270dd47a2ec9b31645f03cdf10e8b196b28a068c03ee

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.