Erdős problem 891
Let be the primes and . Is it true that, for all sufficiently large , there must exist an integer in with many prime factors?
Sources
FormalConjectures/ErdosProblems/
891.lean
Retained formal statement
Let be the primes and . Is it true that, for all sufficiently large , there must exist an integer in with many prime factors?
True ↔ ∀ k ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m ∈ Finset.Ico n (n + ∏ i ∈ Finset.range k, Nat.nth Nat.Prime i), k < ArithmeticFunction.cardDistinctFactors mOpenStatement only, no proof