Skip to content

Erdős problem 1093

Start work

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1093.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/1093.leanErdos1093.erdos_1093.parts.ii4 linesExact file
{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
OpenStatement only, no proof