Skip to content

Erdős problem 890

A question of Erdős and Selfridge [ErSe67], who observe that lim inf⁡n→∞∑0≤i<kω(n+i)≥k+π(k)−1\liminf_{n\to \infty}\sum_{0\leq i < k}\omega(n+i)\geq k+\pi(k)-1 for every kk. This follows from Pólya's theorem that the set of kk-smooth integers has unbounded gaps - indeed, n(n+1)⋯(n+k−1)n(n+1)\cdots (n+k-1) is divisible by all primes ≤k\leq k and, provided nn is large, all but at most one of n,n+1,…,n+k−1n,n+1,\ldots,n+k-1 has a prime factor >k>k by Pólya's theorem.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

890.lean

Retained formal statement2 of 4

Is it true that lim sup⁡n→∞(∑0≤i<kω(n+i))log⁡log⁡nlog⁡n=1,\limsup_{n\to \infty}\left(\sum_{0\leq i < k}\omega(n+i)\right) \frac{\log\log n}{\log n}=1, where ω\omega counts the number of distinct prime factors without restriction?

FormalConjectures/ErdosProblems/890.leanErdos890.erdos_890.parts.b8 linesExact file
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 =      1
OpenStatement only, no proof