---

Claim. Let $\delta(m,\alpha)$ be the density of the integers divisible by some $d\equiv1\pmod m$ with $1<d<\exp(m^\alpha)$. Then $\lim_{m\to\infty}\delta(m,\alpha)$ is $0$ for every $\alpha<1/\log2$ and $1$ for every $\alpha>1/\log2$. The threshold $\beta$ the problem asks for exists and equals $1/\log2$, so the question is answered in the affirmative.

Source. R. R. Hall, On some conjectures of Erdős in Astérisque, I, Journal of Number Theory 42 (1992), no. 3, 313--319, doi:10.1016/0022-314X(92)90096-8; the issue is dated November 1992, which names this page. The paper is not held in the library; the statement above is the one the site records for it, and it matches the conjecture Erdős states on p. 81 of Er79e, where he also writes that he can prove $\delta(m,1)\to0$.

Acceptance. Refereed: the paper appeared in the Journal of Number Theory. Reviewed: the site's curator, Thomas Bloom, marks Problem 697 proved and credits Hall's paper with the affirmative answer and the value $\beta=1/\log2$.

Formalization. The Lean file Erdos697.lean in Boris Alexeev's repository of Lean proofs, linked above at the commit of 2026-09-04 that last touched it, declares itself a formalization of a solution to Problem 697 with Hall as its informal author and Codex and GPT-5.6 Sol as its formal authors. Its theorem erdos_697 states that $1<1/\log2$, that $\delta(m,\alpha)\to0$ for every $\alpha<1/\log2$ and that $\delta(m,\alpha)\to1$ for every $\alpha>1/\log2$, which is the claim above; the file was added on 2026-08-16 and strengthened to the exact threshold on 2026-08-23. Because the file declares itself a formalization of Hall's result, it is a link on this page and not a claim of its own; this corpus has not built or audited it, so the page lists no formalized evidence.