The board / number theory / #682
Erdős Problem #682
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The `n`th prime, indexed from zero: `p 0 = 2`, `p 1 = 3`, ...
Is it true that for almost all \(n\) there exists some \(m\in (p_n,p_{n+1})\) such that \[p(m) \geq p_{n+1}-p_n,\] where \(p(m)\) denotes the least prime factor of \(m\)? This was solved in the affirmative by Gafni and Tao [GaTa25]. This was formalized in Lean by Codex and GPT-5.6 Sol.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/682.Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA386978
Original pageerdosproblems.com/682
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.