Covering $[1,n]$ by residues of only the large primes: estimate $\epsilon_n$; is $\epsilon_n=o(1)$? (Erdős #688)
Statement
Define $\epsilon_n$ to be maximal such that there exists a choice of congruence class $a_p$ for every prime $n^{\epsilon_n}<p\leq n$ with the property that every integer in $[1,n]$ satisfies at least one of the congruences $\equiv a_p\pmod p$. Estimate $\epsilon_n$. In particular, is it true that $\epsilon_n=o(1)$?
Acceptance. FULLY RESOLVES (proof-shaped): a complete rigorous proof — a Lean/Coq formalisation preferred, otherwise a full written proof — of an asymptotic estimate for $\epsilon_n$, in particular settling whether $\epsilon_n=o(1)$. ADVANCES: improve the lower bound stated in the background ($\epsilon_n\gg \log\log\log n/\log\log n$, Erdős) with proof; establish any nontrivial upper bound on $\epsilon_n$ with proof; or compute $\epsilon_n$ rigorously for a new record range of $n$ with a reproducible, exhaustively-certified search program. Deliver the proof, the improved bound, or the search code plus certified values.
Background
Posed by Erdős [Er79d, Er80] and listed as open on erdosproblems.com/688 (fetched 2026-07-21, status 'open'). This is a companion to the Jacobsthal-type covering problem Erdős #687 (erdosproblems.com/687) and to Erdős #689 (erdosproblems.com/689); it asks how narrow a band of primes — only those exceeding $n^{\epsilon_n}$ — can still sieve out all of $[1,n]$. Erdős established the lower bound $\epsilon_n\gg \frac{\log\log\log n}{\log\log n}$. Whether $\epsilon_n\to 0$ (i.e. $\epsilon_n=o(1)$) is open. A formalised statement of this problem exists in the DeepMind formal-conjectures repository. See also Erdős #1200 (erdosproblems.com/1200). Attacker's tool: sieve / covering-density estimates matching the prime-gap machinery of Ford–Green–Konyagin–Maynard–Tao, together with direct computation of $\epsilon_n$ for small $n$ to reveal its trend.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #688 (T. F. Bloom) | website |
| REF-02 | Lean formalisation (DeepMind formal-conjectures) #688 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.