Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 248

../

claims/: The 2 claim pages of Problem 248, one per claimant's result; the problem's standing derives from them.


Statement. Are there infinitely many nn such that, for all k≥1k\geq 1,

ω(n+k)≪k?\omega(n+k) \ll k?

(Here ω(n)\omega(n) is the number of distinct prime divisors of nn.)

Status. PROVED (LEAN), the site's label (page last edited 2026-04-17). The site's curator records the problem as resolved by Tao and Teräväinen [TaTe25] and credits Lau [La26] with improving the bound to ω(n+k)≪log⁡k\omega(n+k)\ll\log k for k≥2k\ge2, a bound that after the shift n↦n+1n\mapsto n+1 answers the question as posed by itself; the formal-conjectures project links a Lean proof of the full statement. The two accepted claims are Tao and Teräväinen 2025 and Lau 2026.

Source. erdosproblems.com/248, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #248, https://www.erdosproblems.com/248.

References.

  • [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
  • [La26] C. F. Lau, On the number of prime factors of consecutive integers. arXiv:2604.15042 (2026).
  • [TaTe25] T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers. arXiv:2512.01739 (2025).

Formalization. Statement in formal-conjectures (at its commit of 2026-09-18; erdos_248, category research solved), which links as its formal proof the Lean 4 file Erdos248.lean of the lean-proofs repository; the claim page records its attribution. This corpus has built and audited neither file.

Current assessment

Proved; two accepted full claims on the site's curator's record. The site formulation above (page last edited 2026-04-17) asks for infinitely many nn with ω(n+k)≪k\omega(n+k)\ll k for all k≥1k\ge1. Tao and Teräväinen prove it with an absolute constant, and the site records the problem as resolved by them. Lau's Ω(n+k)≤Clog⁡k\Omega(n+k)\le C\log k for every k≥2k\ge2, which the site credits as an improvement, also settles the question by itself: for n′=n+1n'=n+1 and every j≥1j\ge1, ω(n′+j)≤Ω(n+(j+1))≤Clog⁡(j+1)≤Cj\omega(n'+j)\le\Omega(n+(j+1))\le C\log(j+1)\le Cj. Neither preprint is known to be refereed, and the Lean development that formal-conjectures links as the formal proof has not been built or audited by this corpus, so both standings rest on the curator's documented acceptance. Erdős and Graham [ErGr80] had written that too little was known about sieves to handle the question. The site relates the problem to Problems 69, 679 and 826.

The discussion thread's one other proof-shaped post, of 2025-12-01, links a dated manuscript, John N. Dvorak's A Probabilistic Sieve Framework for Linearly Bounded Prime Factors (2025-11-30), and a Lean file, Erdos248_Hybrid_Sieve_Framework.lean, which the post says was completed with the AI systems Aristotle, Google Gemini and Kimi K2. The Lean file proves, from axioms it declares (Selberg–Delange-type Markov bounds, a geometric tail bound and combinatorial counting statements), that a core density hypothesis HcoreH_{\mathrm{core}} implies infinitely many nn with the required bound, and the post says that it does not claim a solution. The same day the author conceded that the hypothesis fails for this problem, the core density, about exp⁡(−(log⁡log⁡N)2)\exp(-(\log\log N)^2), being swallowed by the tail's polynomial error term. The implication therefore decides nothing, and the post gets no claim page.

Search scope (2026-10-07): the site's page and discussion thread (six comments, 2025-10-19 to 2026-04-17), the formal-conjectures statement file at its 2026-09-18 commit, the lean-proofs file and its commit history, and the arXiv records of both preprints.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.