Erdős problem 386
There is a , such that and can be the product of consecutive primes infinitely often?
Sources
FormalConjectures/ErdosProblems/
386.lean
Retained formal statement
For all , can be the product of consecutive primes infinitely often?
True ↔ ∀ k ≥ 2, ∃ᶠ (n : ℕ) in Filter.atTop, k ≤ n - 2 ∧ ∃ p q, n.choose k = ∏ i ∈ Finset.Ico p q, Nat.nth Nat.Prime iOpenStatement only, no proof