Documentation

FormalConjectures.ErdosProblems.«386»

Erdős Problem 386 #

Reference: erdosproblems.com/386

theorem Erdos386.erdos_386 :
sorry k2, ∃ᶠ (n : ) in Filter.atTop, k n - 2 ∃ (p : ) (q : ), n.choose k = iFinset.Ico p q, Nat.nth Nat.Prime i

Let $2 \le k \le n - 2$. Can $\binom{n}{k}$ be the product of consecutive primes infinitely often?