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
It is a classical fact that
Filter.limsup (fun n => ↑(ArithmeticFunction.cardDistinctFactors n) * (↑(Real.log (Real.log ↑n)) / ↑(Real.log ↑n))) Filter.atTop = 1SolvedStatement only, no proof