A Linear-Scale Solution to Erdős Problem 450

The problem and its hidden difficulty

Erdős asked how large an interval length $y=y(\epsilon,n)$ must be before the integers in $(x,x+y)$ having a divisor in $(n,2n)$ occupy at most an $\epsilon$-fraction of the interval.

The natural uniform reading is adversarial in the translate: the estimate must hold for every $x$, not merely for a typical interval. That distinction is the main difficulty. Global density estimates—even very strong ones—do not prevent exceptional translates from containing dense clusters.

There is also a genuine linear obstruction. Immediately after a suitable factorial translate, an interval of length $n$ contains $n-1$ qualifying integers. Thus no answer of order $o(n)$ can work for fixed $0<\epsilon<1$. The real question is whether one can prove a matching $O_\epsilon(n)$ upper bound uniformly in $x$.

Where the earlier routes stalled

The first exact approach used periodicity. For fixed $n$, divisibility by some $d\in(n,2n)$ is periodic, so the problem has a precise period-density criterion. This led to a complete fixed-$n$ dichotomy: an eventual threshold exists exactly when $\epsilon$ exceeds the density in one period.

That result was correct but did not solve the asymptotic problem. Its period is enormous, and it left open the essential assertion that the density tends to zero with $n$.

A Möbius expansion improved the local discrepancy dramatically, replacing the full period by a subexponential coefficient norm. But this route still needed a formally imported global multiplication-table theorem, such as Ford's deep density estimate. More importantly, it obscured the simpler structure needed for a linear bound.

The conceptual mismatch was this: global density machinery was being asked to solve a local, adversarial-translate problem. What was needed instead was a statistic that both concentrates on every long enough interval and behaves predictably when a bad integer is factored as $m=dk$.

The key breakthrough: finite-prime scores

Fix a finite set $S$ of primes, all at least five, and define

$$U(m)=\#\{p\in S:p\mid m\}.$$

A second, two-level score also records repeated selected prime factors:

$$W(m)=U(m)+\#\{p\in S:p^2\mid m\}.$$

The decisive pointwise inequality is

$$U(d)+U(k)\le W(dk).$$

If a selected prime divides both factors, its second occurrence is exactly what the $p^2$-term records. This turns the factorization $m=dk$, with $n<d<2n$, into a usable local trichotomy.

Let

$$\mu=\sum_{p\in S}\frac1p, \qquad Q=\prod_{p\in S}p^2.$$

Both scores are periodic modulo $Q$. Exact first and second moments over a complete period give

$$\sum_{m<Q}(U(m)-\mu)^2\le Q\mu.$$

Chebyshev's inequality therefore controls integers with unusually low score. A Markov estimate for square divisibility controls integers with unusually high two-level score. Periodicity transfers these estimates to every interval, with only one fixed period of boundary loss.

The three-class decomposition

For every bad integer $m$, choose a divisor $d\in(n,2n)$ and write $m=dk$. Then at least one of the following holds:

1. $U(d)\le 3\mu/4$;
2. $U(k)\le 3\mu/4$;
3. $W(m)\ge 3\mu/2$.

Indeed, if the first two alternatives fail, the product inequality forces the third.

The three classes can be counted uniformly in the translate. Once $Q\le n$ and $y\ge n(Q+2)$, their weighted contributions are at most

• $64y$ for low-score divisors;
• $32y$ for low-score quotients;
• $56y$ for high two-level score.

Thus

$$\#\{m\in(x,x+y):m\text{ has a divisor in }(n,2n)\}\,\mu\le 152y$$

for every $x$.

The sum of the reciprocals of the primes diverges, so for each $\epsilon>0$ one may choose a finite $S_\epsilon$ with $\mu>152/\epsilon$. The preceding inequality then gives the desired $\epsilon y$ bound at the linear scale $n(Q_\epsilon+2)$.

Why the order is sharp

The factorial dense block supplies the matching lower obstruction. At length $y=n$, one explicit translate has exactly $n-1$ bad integers. For every fixed $0<\epsilon<1$, this violates the requested estimate for all sufficiently large $n$.

Consequently, every sufficient eventual threshold must exceed $n$ eventually, while the finite-prime argument gives a constant multiple of $n$. The optimal fixed-$epsilon$ growth order is therefore $\Theta_\epsilon(n)$.

Formal verification

The complete argument was formalized in Lean 4 with Mathlib. The formal statement uses open intervals, natural translates, the real inequality “at most $\epsilon y$,” and requires the estimate for every length above the threshold.

The main theorem is:

theorem turanLinearAnswer_isSufficientScale :
    IsSufficientScale turanLinearAnswer

A second theorem proves the matching eventual lower bound for every $0<\epsilon<1$.

The hostile checker rejects sorry, admit, local axioms, and unsafe declarations before building the standalone proof project. It reports:

Build completed successfully (8567 jobs).
PASS: Lean build succeeded and local sources contain no forbidden escape hatch

The proof is archived in verified_math/F-013_turan-linear-scale/.