---

Claim. There is an infinite sequence $A=\{n_1<n_2<\cdots\}$ of positive integers with

$$\lim_{N\to\infty}\frac1N\sum_{k\le N}\frac{\phi_A(k)}{n_k}=0,$$

where $\phi_A(k)$ counts the $1\le m\le n_k$ whose fraction $m/n_k$ in lowest terms has a denominator different from every earlier $n_j$. This answers Problem 1000 yes, against the expectation Erdős recorded in 1964, when he could show only that $\phi_A(k)/n_k$ cannot tend to zero and that a zero lower limit forces an upper limit of one. Cassels had shown in 1950 that the lower limit of the average can be zero for his count, which excludes every $m$ whose reduced denominator divides an earlier term (card cassels_1950); the question asks for the full limit. The result is in J. A. Haight, Metric Diophantine Approximation and Related Topics, PhD thesis, University of London, Westfield College, dated February 1971 on its title page (the catalog's entry [Ha] gives no year). The site's thread describes the construction as Cassels's construction combined with a multiplication of the sequence, and the Lean file below builds the sequence from blocks of multiples of a large prime by the divisors of a primorial.

The claim is stated in the site's count, which never falls below Cassels's, the count of Erdős's question [Er64b, p. 59], so it also answers that question. The thread's account rests on the average being unchanged when a sequence is multiplied by a constant, which holds for Cassels's count but not for the site's (for the sequence $1,2$ the second ratio is $1/2$ under both counts; for $2,4$ it is $1/2$ under Cassels's and $3/4$ under the site's); the site's version is the one the Lean file below proves, by its own construction.

Acceptance. The reviewed evidence is the documented acceptance by the catalog erdosproblems.com, whose page carries the label PROVED (LEAN), last edited 2025-12-05, and whose curator, Thomas Bloom, credits Haight with the proof that such a sequence exists. The thread (second discussion link) carries the posts of 2025-12-04 that identified the thesis (its Chapter 2) as the solution, said that Erdős mentions the solution on p. 5 of his 1975 paper Problems and results on diophantine approximations (II), and noted that ChatGPT helped locate the reference. No refereed journal version is known; the thesis is a doctoral dissertation, and no refereed evidence is listed.

Formalization. A third party formalized the solution: thm_main in src/v4.29.1/ErdosProblems/Erdos1000.lean of https://github.com/plby/lean-proofs, pinned above at the commit of 2026-06-24, the file's version of that date (the proof entered the repository on 2025-12-28). The file declares itself a formalization of a solution to the problem, names Haight and ChatGPT as informal authors and Aristotle and Boris Alexeev as formal authors, so it is a link on this page rather than an independent claim. Its theorem gives a strictly increasing $n:\mathbb N\to\mathbb N$ with $\frac1N\sum_{k=1}^N\phi_A(k)/n_k\to0$, with $\phi_A$ defined by the problem's condition $n_k/\gcd(m,n_k)\ne n_j$; it imports only Mathlib and contains no sorry. The formal-conjectures catalog (the record link, pinned to the commit of 2026-09-18 that last touched its file) tags its own statement erdos_1000 as research solved and cites this file as the formal proof; its definition uses non-divisibility $n_k/\gcd(m,n_k)\nmid n_j$, Cassels's count, to which the catalog corrected its earlier inequality on 2026-09-13; since that count never exceeds the site's, the linked proof of the site's version implies the catalog's statement. This repository has not built the file, printed its axioms or audited its definitions against the problem, so the claim carries no formalized evidence and the site's "(LEAN)" qualifier is reported, not warranted, here.

Depends on. Nothing in this wiki.