Erdős Problem 386

Reference: erdosproblems.com/386

theorem Erdos386.erdos_386 : sorry ↔ ∃ k ≥ 2, ∃ᶠ (n : ℕ) in Filter.atTop, k ≤ n - 2 ∧ ∃ (p : ℕ) (q : ℕ), n.choose k = ∏ i ∈ Finset.Ico p q, Nat.nth Nat.Prime i

There is a $k$, such that $2 \le k \le n - 2$ and $\binom{n}{k}$ can be the product of consecutive primes infinitely often?

theorem Erdos386.erdos_386.variants_forall : sorry ↔ ∀ k ≥ 2, ∃ᶠ (n : ℕ) in Filter.atTop, k ≤ n - 2 ∧ ∃ (p : ℕ) (q : ℕ), n.choose k = ∏ i ∈ Finset.Ico p q, Nat.nth Nat.Prime i

For all $2 \le k \le n - 2$, can $\binom{n}{k}$ be the product of consecutive primes infinitely often?

theorem Erdos386.erdos_386.variants_two : sorry ↔ ∃ᶠ (n : ℕ) in Filter.atTop, 2 ≤ n - 2 ∧ ∃ (p : ℕ) (q : ℕ), n.choose 2 = ∏ i ∈ Finset.Ico p q, Nat.nth Nat.Prime i

Can $\binom{n}{2}$ be the product of consecutive primes infinitely often?