Erdős problem 890
A question of Erdős and Selfridge [ErSe67], who observe that for every . This follows from Pólya's theorem that the set of -smooth integers has unbounded gaps - indeed, is divisible by all primes and, provided is large, all but at most one of has a prime factor by Pólya's theorem.
Sources
FormalConjectures/ErdosProblems/
890.lean
Retained formal statement
If counts the number of distinct prime factors of which are , then is it true that, for every ,
sorry ↔ ∀ k ≥ 1, Filter.liminf (fun n => ∑ i ∈ Finset.range k, ↑(Erdos890.omegaGt k (n + i))) Filter.atTop ≤ ↑kOpenStatement only, no proof