---

Claim. Call the index $n$ exceptional when no integer $m$ with $p_n<m<p_{n+1}$ has least prime factor $p(m)\geq p_{n+1}-p_n$. Theorem 1.1 of Gafni and Tao bounds the number of exceptional $n$ with $p_n\in[X,2X]$ by $O(X/(\log X)^2)$. Summing over dyadic ranges, the exceptional $n\leq N$ number $O(N/\log N)$, a proportion $O(1/\log N)$ as the paper notes, which is $o(N)$, so the exceptional set has density zero and the question of Problem 682 has the answer yes: for almost all $n$ some $m\in(p_n,p_{n+1})$ has $p(m)\geq p_{n+1}-p_n$. The method is a moment computation for the count of rough numbers in short intervals, with the higher moments controlled through the Montgomery–Soundararajan asymptotics for singular series; the second moment alone already gives $O(X/(\log X)^{4/3-o(1)})$ exceptions, enough for the density statement. Under a form of the prime tuples conjecture the paper sharpens the count to $\sim cX/(\log X)^2$ for an explicit constant $c>0$. The paper's digest is the [[../library/primes/gafni_2025_rough_numbers_between_consecutive_primes/_index|source card]].

Whether the "almost all" can be dropped is open. Assuming Schinzel's hypothesis H (Dickson's conjecture suffices for these two linear forms), Erdős showed, in the passage from his 1979 paper that Gafni and Tao quote, that the statement fails for infinitely many $n$: when $2183+30030d$ and $2201+30030d$ are both prime they are consecutive primes, since every integer strictly between them is divisible by one of the primes up to $13$, and each such integer then has least prime factor at most $13$, below the gap $18$. Unconditionally, it is open whether infinitely many gaps contain no such integer (Gafni and Tao, Remark 1.2).

Acceptance. The site's curator, Thomas F. Bloom, marks Problem 682 proved and credits Gafni and Tao's paper for the affirmative answer, the reviewed evidence. The paper is cited as A. Gafni and T. Tao, Rough numbers between consecutive primes, arXiv:2508.06463 (2025), submitted on 8 August 2025, the date of this page; no journal publication is recorded, so no refereed evidence is listed.

Formalization. Erdos682.lean in Boris Alexeev's lean-proofs repository, pinned at the commit of 15 September 2026 in the link, declares itself a formalization of a solution to Problem 682, names Gafni and Tao as its informal authors and Codex and GPT-5.6 Sol as its formal authors, and is the file that the formal_proof attribute of the statement in google-deepmind/formal-conjectures names. Its theorem erdos_682 (line 5018) states that the set of $n$ for which some $m$ strictly between the $n$th and $(n+1)$st primes, indexed from zero, has $p_{n+1}-p_n\leq$ the least prime factor of $m$ has natural density $1$; the file imports the PrimeNumberTheoremAnd project and other developments of the repository, and a text scan of its 5,275 lines found no sorry, axiom, native_decide or admit token. This corpus has not built it, so no formalized evidence is listed, and the formal-conjectures statement file is not a formalization link.

Depends on. Nothing beyond the cited paper.