A Proof of Erdős Problem 394

The problem—and the real obstruction

For positive integers $k,n$, let $t_k(n)$ be the least positive integer $m$ such that

$$n\mid m(m+1)\cdots(m+k-1).$$

Erdős Problem 394 asks two average-order questions. Does some $c>0$ satisfy

$$\sum_{n\le x}t_2(n)\ll \frac{x^2}{(\log x)^c}?$$

And, for every fixed $k\ge2$, is

$$\sum_{n\le x}t_{k+1}(n) =o\!\left(\sum_{n\le x}t_k(n)\right)?$$

The difficulty is not merely that $t_k(n)$ is irregular. Its large values are structurally unavoidable. If $p\ge k$ is prime, then

$$t_k(p)=p+1-k;$$

in particular, $t_2(p)=p-1$. Thus no uniform pointwise saving can prove either assertion. Even the elementary monotonicity $t_{k+1}(n)\le t_k(n)$ is far too weak: the second question asks for a ratio tending to zero after summation.

Both questions nevertheless have affirmative answers. The first estimate holds with the explicit choice $c=1/2048$, and the adjacent sums satisfy the requested little-o relation for every fixed $k\ge2$.

Why the natural attacks stalled

The failed approaches exposed four distinct traps.

• Pointwise estimates attack the wrong phenomenon. Prime inputs keep $t_k(n)$ nearly as large as $n$. The saving exists only after the arithmetic structures of many integers are aggregated.
• An upper-bound sieve proves only half the theorem. It is possible to make the $t_{k+1}$-sum small by sieving medium prime factors, but comparison with $t_k$ also requires a denominator lower bound that preserves a stronger Euler factor.
• Crude Euler estimates destroy the adjacent-length gap. The saving between $k$ and $k+1$ is encoded in a precise powered inequality. Estimating the products separately loses exactly the small exponent difference needed at the end.
• A sparse subsequence does not settle an all-$x$ asymptotic. An early hierarchy at cutoffs $16^{j^D}$ gave valid and strong finite bounds. But neighboring cutoffs were separated by enormous factors, so monotonicity could not interpolate the ratio estimate. The finite work was useful; the grid itself was a dead end.

The conceptual mistake behind the most natural sieve route was therefore to view the numerator as the whole problem. The decisive step was to build the numerator and denominator as a matched pair, retain their exact Euler-product relationship, and place both estimates on a dense multiplicative grid.

The finite numerator mechanism

Fix an adjacent length parameter $K$, a cutoff $X$, and an interval of medium primes $P=(z,y]$. For each $n\le X$, extract the squarefree product $q\mid n$ of the primes from $P$ which divide $n$. Integers divisible by some $p^2$, with $p\in P$, form a controlled exceptional set.

For all remaining integers, admissible starts can be encoded prime by prime. The proof packages these local choices into a finite root box. A lattice-counting and moment argument bounds the mean least admissible start over that box. It then combines this bound with an even Bonferroni truncation and a completely explicit finite Brun sieve.

The result is a global upper bound for

$$S_{K+1}(X)=\sum_{n\le X}t_{K+1}(n),$$

consisting of a sieve-density Euler main term and explicit square-prime and Brun-tail errors. Progression discrepancies, elementary-symmetric tails, and truncation losses are all handled as finite inequalities; no asymptotic sieve theorem is inserted as an unproved black box.

The missing denominator

For a selected squarefree modulus $q$, attach a prime $\ell$ larger than every medium prime and consider $n=q\ell$. Most unit residue classes of $\ell\pmod q$ avoid all short shifted-product representations. For a prime in one of those good classes, the least valid start is forced to be large, giving a lower bound for $t_K(q\ell)$.

A second finite prime sieve lower-bounds the weighted mass of the good primes. These contributions can then be summed over many selected moduli $q$. Because the attached prime $\ell$ lies above the medium-prime range, unique factorization makes

$$(q,\ell)\longmapsto q\ell$$

injective. No denominator mass is counted twice.

After controlling floors and the subset truncation, this construction produces a lower bound for

$$S_K(X)=\sum_{n\le X}t_K(n)$$

with an enhancement factor

$$\prod_{p\in P}\left(1+\frac1{Kp}\right).$$

That enhancement is the feature a generic lower bound misses, and it is precisely what makes adjacent lengths separate.

The key insight: keep the Euler gap exact

The numerator density and denominator enhancement obey an exact powered comparison. With

$$M=(K+1)(2K+1),$$

the relevant products can be arranged into an inequality of the form

$$(A/E)^M\le B^{M+1}.$$

The extra power on the right is the fixed saving. Rather than approximate each product independently, the proof carries this identity intact until elementary reciprocal-prime and endpoint-density estimates turn it into a logarithmic gain.

This is the central mathematical insight of the proof: the little-o statement comes from an algebraic gap between two matched Euler products, not from a stronger standalone estimate for either sum.

The dense hierarchy

To turn the finite estimates into an asymptotic valid at every cutoff, use

$$X_N=16^N, \qquad h=\lfloor\log_2N\rfloor,$$

and choose the lower and upper medium-prime scales using the exponents $h^2$ and $\lfloor N/h^4\rfloor$. A generous polynomial dilution and an even Brun order leave enough room for all root-box, tail, and denominator conditions.

The crucial strengthening is uniformity between grid points. For each fixed $K\ge2$, the formal proof establishes that, eventually in $N$, every natural cutoff satisfying

$$16^N\le X\le16^{N+1}$$

obeys

$$\boxed{ \lfloor\log_2N\rfloor\,S_{K+1}(X) \le 3S_K(X). }$$

Unlike the abandoned sparse hierarchy, this grid has bounded multiplicative gaps, and the estimate already covers each entire gap.

For a large real $x$, take $X=\lfloor x\rfloor_+$ and $N=\lfloor\log_{16}X\rfloor$. Exact natural-logarithm inequalities place $X$ in the required interval. Since $\lfloor\log_2N\rfloor\to\infty$, for every $\varepsilon>0$ it eventually exceeds $3/\varepsilon$. The boxed estimate then gives

$$S_{K+1}(X)\le\varepsilon S_K(X),$$

which is exactly the epsilon definition of the desired little-o relation.

Verification

The proof is formalized in Lean 4 with Mathlib. The formal statement preserves every important detail of the original question:

• t k n is the least positive start;
• the consecutive product is exact natural-number arithmetic;
• Tsum k x sums over Finset.Icc 1 ⌊x⌋₊;
• the conclusions use Mathlib's IsBigO atTop and IsLittleO atTop;
• the second assertion quantifies over every fixed natural $k\ge2$.

The final archive contains 106 Lean source files. Its verifier scans every source for sorry, admit, and added axiom declarations, builds the complete dependency closure, and directly elaborates the file containing both final target theorems. The full build completed successfully, and the definitive output was:

PASS: both faithful Erdős 394 targets are proof-escape-free and accepted by Lean

The source-only closure was also rebuilt during independent review, and Colin accepted the result for publication.