---

Hooley, On the difference between consecutive numbers prime to $n$. II, Publ. Math. Debrecen 12 (1965), 39–49, received 5 December 1963 (the page name's date). Its Theorem 1 states that when $n\to\infty$ along integers with $n/\phi(n)\to\infty$, the gaps $\Delta_i=a_{i+1}-a_i$ between consecutive integers coprime to $n$, divided by their mean $n/\phi(n)$, are asymptotically distributed as a gamma variable with parameter $1$, that is, exponentially: with $f_n(c)$ "the number of intervals for which $\Delta_i<cn/\varphi(n)$" (Theorem 1; the inequality is strict as printed), $f_n(c)=\varphi(n)\{1+o(1)\}(1-e^{-c})$ uniformly for $c$ in any fixed range bounded at both ends by positive constants. The problem's quotient counts the gaps with $\le$ instead; since $f_n(c)\le\#\{i:\Delta_i\le cn/\phi(n)\}\le f_n(c+\varepsilon)$ for every $\varepsilon>0$ and $1-e^{-c}$ is continuous, the proportion of gaps at most $c\,n/\phi(n)$ also tends to $1-e^{-c}$, uniformly on such a range. Hooley names the primorial case $n=2\cdot3\cdots p_k$ of Problem 235 as Erdős's conjecture; since $N_k/\phi(N_k)\to\infty$, the theorem gives that the problem's limit exists for every $c>0$ and equals $1-e^{-c}$ (at $c=0$ no gap is counted and both sides vanish), a continuous function of $c$. The problem's quotient counts the $\phi(N_k)-1$ internal gaps against the denominator $\phi(N_k)$, a difference of one gap that does not affect the limit. The paper's digest is the [[../library/integer_sequences/hooley_1965_difference_between_consecutive_numbers_prime/_index|library card]].

Read depth. The page rests on the printed statement of Theorem 1, checked clause by clause; the proof was not read.

Acceptance. The result is refereed (Publicationes Mathematicae Debrecen), and the site's curator, Thomas Bloom, records the problem as solved by Hooley with the limit $f(c)=(1+o(1))(1-e^{-c})$ (erdosproblems.com/235, page last edited 22 January 2026, as of 2026-10-07); the curator had no part in the result. Nothing here is this project's own review.

Formalization. The file src/latest/ErdosProblems/Erdos235.lean of the public repository plby/lean-proofs, linked at the pinned commit (added 2026-08-17; toolchain comment leanprover/lean4:v4.33.0, Mathlib v4.33.0), declares itself a formalization of Hooley's theorem: its header names Hooley as the informal author and Codex and GPT-5.6 Sol as the formal authors; the repository's ErdosProblems/Erdos235.md calls it a formalized proof of Erdős Problem 235 and names no author. It defines the problem's quotient gapCDF k c for the primorial $N_k$ and proves erdos_235, that a continuous $f:\mathbb R\to\mathbb R$ has gapCDF k c tending to $f(c)$ as $k\to\infty$ for every $c\ge0$, with $f(c)=1-e^{-c}$ supplied by erdos_235_limit; it imports two sibling developments of the repository (a Brun sieve and a congruence-average file) besides Mathlib, prints its axioms with #print axioms and contains no sorry. The file was neither built nor audited here, so it is linked and not counted as formalized, and its statement's fidelity to the problem is not established by this corpus. No outside record registers it: the site shows no formalized statement and no Lean label for the problem, formal-conjectures has no 235.lean, and the community database recorded the problem unformalized on 2025-08-31 (all).