Singmaster's conjecture

Singmaster's conjecture says that for any integer $t>1$, the number of solutions to the equation:

$\binom{n}{k} = t,\quad 1 \le k < n,$

with $\binom{n}{k}$ being the numbers that appear in Pascal's triangle, is bounded by a global constant $O(1)$.

Reference: Wikipedia

def Singmaster.solutions (t : ℕ) : Set (ℕ × ℕ)

The set of pairs (n, k) representing the solutions to the equation Nat.choose n k = t for a given t, under the constraint 1 ≤ k < n.

Equations

• Singmaster.solutions t = {(n, k) : ℕ × ℕ | 1 ≤ k ∧ k < n ∧ n.choose k = t}

theorem Singmaster.singmaster : ∃ (C : ℕ), ∀ t > 1, (solutions t).Finite ∧ (solutions t).ncard ≤ C