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 such that, for all ,
(Here is the number of distinct prime divisors of .)
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 for , a bound that after the shift 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 with for all . Tao and Teräväinen prove it with an absolute constant, and the site records the problem as resolved by them. Lau's for every , which the site credits as an improvement, also settles the question by itself: for and every , . 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 implies infinitely many 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 , 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.