The board / number theory / #235
Erdős Problem #235
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 product of the first `k + 1` primes. On [erdosproblems.com/235](https://www.erdosproblems.com/235) this is \(N_{k+1}=2\cdot 3\cdots p_{k+1}\). The limit as \(k\to\infty\) is the same for either indexing.
The increasing list of integers `< n` that are coprime to `n`.
The gaps \(a_i - a_{i-1}\) between consecutive entries of `coprimeList n`.
Let \(N_k=2\cdot 3\cdots p_k\) and \(\{a_1<a_2<\cdots <a_{\phi(N_k)}\}\) be the integers \(<N_k\) which are relatively prime to \(N_k\). Then, for any \(c\geq 0\), the limit \[\frac{\#\{ a_i-a_{i-1}\leq c \frac{N_k}{\phi(N_k)} : 2\leq i\leq \phi(N_k)\}}{\phi(N_k)}\] exists and is a continuous function of \(c\). Solved by Hooley [Ho65], who proved that these gaps have an exponential distribution: that is, if \(f(c)\) is the function in question, then \[f(c)=(1+o(1))(1-e^{-c})\] (where the \(o(1)\) goes to \(0\) uniformly as \(k\to \infty\)). See also [234](https://www.erdosproblems.com/234) for a more difficult version of this problem using actual primes.
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/235.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/235
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.