The board / number theory / #726
Erdős Problem #726
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
As \(n\to \infty\) ranges over integers \(\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}\)? A conjecture of Erdős, Graham, Ruzsa, and Straus [EGRS75]. By \(n\in (p/2,p)\pmod{p}\) we mean \(n\equiv r\pmod{p}\) for some integer \(r\) with \(p/2<r<p\). The remainder `n % p` is computed in `ℕ` before casting to `ℝ`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/726.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/726
Attempts
submit one →Read our working report →
Rigorous modulo MRSTT Proposition 1.13, \(1/6\leq\liminf S(n)/\log\log n\leq\limsup S(n)/\log\log n\leq5/6\); exhaustive rational enclosures verified every \(100\leq n\leq10^7\), but the uniform recip
PARTIAL