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
Is it true that where counts the number of distinct prime factors without restriction?
sorry ↔ ∀ k ≥ 1, Filter.limsup (fun n => (∑ i ∈ Finset.range k, ↑(ArithmeticFunction.cardDistinctFactors (n + i))) * (↑(Real.log (Real.log ↑n)) / ↑(Real.log ↑n))) Filter.atTop = 1OpenStatement only, no proof