---

Claim. For a set $A$ of positive integers write $T(A)$ for the sum of $1/(a_2-a_1)$ over all pairs $a_1<a_2$ in $A$ and $S(A)$ for the same sum over consecutive pairs only. Daniel Larsen's note "A question of Erdős on reciprocals of gaps between divisors" proves that

$$\frac{T(\operatorname{div}(n))}{1+S(\operatorname{div}(n))}$$

is unbounded as $n$ ranges over the natural numbers, where $\operatorname{div}(n)$ is the set of divisors of $n$. This is the negation of the problem's inequality with an absolute implied constant, so the answer to the question is no. The proof takes Tao's construction, a product of primes lying in a short window with nearly even spacing, and repeats it on many widely separated scales: at a single scale the primes can be produced unconditionally by a sieve and pigeonhole argument at the cost of a smaller window, which keeps the ratio of $T$ to $S$ large but no longer makes $T$ large compared with $1$; stacking scales accumulates $T$ while preserving the ratio, and elementary estimates bound the cross-scale contributions to $S$. The manuscript was posted in the author's repository on 27 March 2026, announced on the problem's forum on 29 March 2026, and revised on 30 March 2026 after comments; the link is pinned to the revised file. Its Proposition 2.1 adapts the key estimate of Tao's note, and its proof uses that note's Lemma 2.2, an unconditional lower bound on the constant difference of two root-product polynomials; it does not use the prime tuples hypothesis.

Acceptance. The site's curator, Thomas Bloom, records in the problem's remarks that Larsen disproved the statement unconditionally and labels the problem disproved, the reviewed evidence listed here. The note is not refereed.

Depends on. No page of this wiki.

Formalization. The repository at the second link declares itself a formalization of Larsen's proof: its main theorem, Erdos884.erdos_884_disproof, is the negation of the formal-conjectures statement for the problem, with that file's two definitions reproduced verbatim and its ≪ read as =O[Filter.atTop]. Its README says it was formalized by Claude Fable 5 with guidance from R. J. Honicky, orchestrating parallel prover agents against a hosted verification service, in July 2026; that the amalgamated file is about 8,500 lines, builds with no sorry and the axioms propext, Classical.choice and Quot.sound alone; that it vendors the Selberg sieve from the Apache-2.0 project PrimeNumberTheoremAnd; and that it deviates from the paper in proof-preserving ways (a wider prime window to use Mathlib's Chebyshev bounds, an elementary replacement for the dyadic-shell count, and a greedy scale recursion in place of the exponential tower). The repository's commits are dated 4 July 2026, the date of the link above; the posting on the problem's forum of 5 July 2026 brought it to the site, the change marking the problem Lean-disproved in the site's community database was proposed on 4 July and merged on 17 July 2026, and the site's label DISPROVED (LEAN) rests on it. This corpus has not built it, so no formalized evidence is listed.