The board / number theory / #457
Erdős Problem #457
PROVED LEANdatabase updated 2026-03-07
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Is there some \(\epsilon > 0\) such that there are infinitely many \(n\) where all primes \(p \le (2 + \epsilon) \log n\) divide \[ \prod_{1 \le i \le \log n} (n + i)? \] This was formalized in Lean by Baretto and van Doorn using Aristotle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/457.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA391668
Original pageerdosproblems.com/457
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.