A Positive Answer to Erdős Problem 489

The problem—and the hidden difficulty

Let $A\subseteq\mathbb N$ be extremely sparse,

$$|A\cap[1,x]|=o(\sqrt x),$$

and let $B=\{b_1<b_2<\cdots\}$ be the positive integers divisible by no member of $A$. Erdős asked whether

$$\frac1x\sum_{b_i<x}(b_{i+1}-b_i)^2$$

always has a finite limit.

At first sight this resembles a routine finite-sieve approximation. Any sieve using only finitely many forbidden divisors is periodic, so its gap statistics have exact limiting averages. Sparse $A$ also forces the reciprocals of its increasing enumeration to be summable. Neither observation is enough: the expression is a second moment, and a tiny amount of mass can escape to increasingly long gaps. Pointwise convergence of every fixed gap-length contribution does not justify exchanging a limit with the infinite sum.

That uniform-integrability obstruction is the real content of the problem.

Where the natural approaches stalled

Several plausible routes fail at exactly this boundary.

• Take larger finite periodic sieves and pass to the limit. This controls every bounded gap pattern, but not the squared mass of gaps whose lengths grow with the cutoff. We formalized an abstract escaping-mass counterexample to this limit-exchange step.
• Sum shifted CRT estimates term by term. Counting one congruence class costs a harmless endpoint error, but paying that error independently for every divisor pair and every shift produces a divergent rank error.
• Use a stronger reciprocal moment. A direct incidence argument works under an extra hypothesis such as $\sum r/a_r<\infty$, where $a_r$ is the forbidden enumeration. That misses the sharp regime allowed by $a_r/r^2\to\infty$, including the logarithmic boundary models that make the problem difficult.
• Rely only on a maximum-gap estimate. Thinness does prevent gaps comparable with the whole prefix eventually, but this alone gives no summable control of the collective squared tail.

The successful proof therefore needed two ingredients at once: a global charge for long gaps that does not accumulate CRT endpoint errors, and a separate finite-word argument for bounded gaps.

The breakthrough: charge primitive coprime witness pairs

Write the infinite forbidden set increasingly as $a_0<a_1<\cdots$. Thinness gives three crucial consequences:

1. eventually $(r+1)^2\le a_r$;
2. $\sum_r 1/a_r<\infty$;
3. the rank-pair kernel

$$\sum_{r,s}\frac{\min(r+1,s+1)}{a_ra_s}$$

is summable, with uniformly small high-rank tails.

The task is to make every long actual gap pay into this kernel.

A Mertens-free affine sieve

Inside a long covered gap, we look only at positions

$$n\equiv1\pmod Q,$$

where $Q=Y!$ for a suitably chosen roughness threshold $Y$. This coordinate change has two decisive effects.

• Any forbidden modulus sharing a prime factor with $Q$ is automatically unable to divide such an $n$.
• For the remaining moduli, affine finite-sieve density is the same periodic product density as in the ordinary sieve.

Thus no Mertens estimate is needed. The loss of density contributes a factor $Q^{-1}$, while the bad-pair estimate below gains exactly $Q^{-2}$; those powers cancel after squaring the candidate density.

A uniform interval-density lemma supplies linearly many affine candidates in every sufficiently long gap. Because the reciprocal mass of remote forbidden ranks is small, a divisor-label counting inequality

$$|S|\le G\sum_{r\in\mathrm{labels}(S)}\frac1{a_r}+|\mathrm{labels}(S)|$$

forces linearly many distinct high-rank divisor witnesses.

Quadratically many coprime pairs

Among affine positions, pairs with a common prime divisor are rare. A common prime $p>Y$ forces their difference to be divisible by $Qp$, so each prime fiber is widely spaced. Summing the exact fiber bounds shows that the linearly many witnesses contain quadratically many ordered pairs of coprime positions. Quantitatively, each long gap of length $G$ receives enough pairs to pay for $G^2$ with one fixed constant.

Coprimality is the key structural move. If positions labelled by $a_r,a_s$ are written as

$$n=a_ru, \qquad m=a_sv,$$

then coprimality of $n,m$ makes the quotient vector $(u,v)$ primitive. Repeated scalar dilations—the obstruction that defeated the naive pair count—disappear.

Primitive-ray capacity and global charging

For fixed labels $(r,s)$, all quotient vectors lie in a thin diagonal strip: their covered coordinates are bounded by the prefix, while their difference is bounded by the gap length. Sorting primitive lattice rays by slope and summing consecutive determinants gives a sharp fan-area estimate. In formal cross-multiplied form, the number of possible occurrences satisfies

$$a_ra_s\,\mathrm{capacity} \le 4XC\min(r+1,s+1)+2a_ra_s.$$

Distinct successive gaps inject into distinct quotient pairs, so this is a global capacity bound rather than a separate CRT estimate for each gap. Summing all pair payments yields

$$\sum G^2 \le K\left( X\sum_{(r,s)\in J} \frac{\min(r+1,s+1)}{a_ra_s} + |J| \right).$$

The first term is uniformly small for high ranks by kernel summability. The endpoint term $|J|$ is at most the square of the forbidden counting function, hence is $o(X)$. A witness-forced maximum-gap lemma ensures all charged coordinates lie below a controlled multiple of the prefix. Together these facts prove uniform integrability of the actual squared gaps: for every $\varepsilon>0$, some $H$ makes the normalized contribution of all gaps at least $H$ eventually smaller than $\varepsilon$.

From uniform tails to an actual limit

Long-gap control solves only half the problem. For a fixed cutoff $H$, define a local word cost at an integer $n$: it is $d^2$ when a sieve gap of length $d<H$ starts at $n$, and zero otherwise. Summing these local costs over $[0,x)$ is exactly the sum of squared enumerated gaps shorter than $H$.

A finite forbidden prefix makes this local word periodic, so its normalized average converges to its one-period mean. The full sieve and a sufficiently remote finite prefix disagree on few points: a canonical tail divisor labels every disagreement, and the same reciprocal-mass inequality bounds their density by

\text{tail reciprocal mass}+rac{A(x)}x.

Only starts whose length-$H$ window meets such a disagreement can change their local cost. Therefore every fixed truncated full-sieve average is eventually approximated arbitrarily well by a convergent periodic average, and hence converges.

Finally, the exact gap sum is the truncated average plus its long-gap tail. Applying the same uniform-approximation principle a second time gives convergence of the full normalized second moment.

Finite forbidden sets require a small separate argument: the sieve is periodic after the initial point, every gap is at most one product period, and a shifted periodic Cesàro average converges.

Formal verification

The proof was formalized in Lean 4.31.0 against Mathlib revision fabf563a7c95a166b8d7b6efca11c8b4dc9d911f. It proves the exact statement audited in check_answer/README.md, including the original inclusive counting function, the Nat.nth gap enumeration, and real squared differences.

Two independent project builds passed:

cd workspace/experiments/experiment_1_formal_statement/lean
PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH" LEAN_NUM_THREADS=28 lake build
# Build completed successfully (8618 jobs).

The archival package contains the complete dependency closure:

cd verified_math/F-061_erdos-489-positive-answer
PATH="$HOME/.elan/bin:$PATH" lake update
LEAN_NUM_THREADS=28 lake build
# Build completed successfully (8608 jobs).

A source audit also found no sorry or admit in the F-061 Lean files. The independent referee reran the verification, checked statement fidelity, and accepted the solution.