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
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.
∀ (k : ℕ), Filter.liminf (fun n => ∑ i ∈ Finset.range k, ↑(ArithmeticFunction.cardDistinctFactors (n + i))) Filter.atTop ≥ ↑k + ↑k.primeCounting - 1SolvedStatement only, no proof