Erdős Problem #890

The question

erdos_890.parts.a. If ${\omega }_k(n)$ counts the number of distinct prime factors of $n$ which are $>k$, then is it true that, for every $k\ge 1$, $$\underset{n\to \infty }{\mathrm{liminf}}\sum _{0\le i<k}{\omega }_k(n+i)\le k?$$

erdos_890.parts.b. Is it true that $$\underset{n\to \infty }{\mathrm{limsup}}\left(\sum _{0\le i<k}\omega (n+i)\right)\frac{\log \log n}{\log n}=1,$$ where $\omega$ counts the number of distinct prime factors without restriction?

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«890» (2 statements).

theorem erdos_890.parts.a :
    ∀ k ≥ 1, liminf (fun n ↦ (∑ i ∈ range k, (ω_gt k (n + i) : EReal))) atTop ≤ k

theorem erdos_890.parts.b :
    ∀ k ≥ 1, limsup (fun n ↦ (∑ i ∈ range k, (ω (n + i) : EReal)) *
      (log (log n) / log n)) atTop = 1

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/890. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/890
• [ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.