Erdős Problem 1093

Reference: erdosproblems.com/1093

noncomputable def Erdos1093.deficiency (n k : ℕ) : ℕ

If defined, the deficiency is the count of $0 \le i < k$ such that $n - i$ is $k$-smooth.

Equations

• Erdos1093.deficiency n k = {i ∈ Finset.range k | n - i ∈ k.smoothNumbers}.card

theorem Erdos1093.erdos_1093.parts.i : sorry ↔ {x : ℕ × ℕ | have k := x.1; have n := x.2; 2 * k ≤ n ∧ deficiency n k = 1 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ n.choose k → k < p}.Infinite

Are there infinitely many binomial coefficients with deficiency 1?

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

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