A Formal Proof of Erdős Problem #254

The problem and why it is difficult

Let A ⊆ ℕ. Assume that the number of elements of A in every dyadic shell (x,2x] tends to infinity, and that

$$\sum_{n\in A}\|\theta n\|=\infty$$

for every 0<θ<1, where ‖x‖ is distance to the nearest integer. Erdős asked whether these two hypotheses force every sufficiently large integer to be a sum of distinct elements of A.

The hypotheses control two very different phenomena:

• dyadic abundance gives enough additive growth to build sets of subset sums with bounded gaps;
• phase divergence excludes rational and irrational Bohr obstructions.

Neither condition alone is close to sufficient. The real difficulty is to assign disjoint elements of A to several roles—two piecewise-Bohr classes, a phase-correction class, and a final syndetic class—without destroying the phase hypothesis or reusing a summand.

Where the natural approaches stalled

Several tempting shortcuts are false.

• Coloring dyadic shells and selecting one “good” color does not preserve every phase. Convergent phases form an additive subgroup, but an intersection of four such subgroups can be irredundant. Thus full divergence for the union does not imply full divergence for one color.
• Shell-local reserve choices can be defeated after the fact. A concrete four-point shell shows that every one-point reserve can be made the unique nonmultiple of a suitably chosen modulus.
• Finite modular coverage is not enough. We proved exact tail subset-sum coverage modulo every integer, but irrational Bohr obstructions remain.
• Choosing correction supports after constructing the Bohr system is circular. Enlarging an interval to accommodate corrections moves the base representations and can reintroduce collisions.
• Merely rerunning the standard ergodic proof was not practical. The usual Bergelson–Furstenberg–Weiss proof passes through a symbolic system and its Kronecker factor, infrastructure not already available in Mathlib.

The key was therefore to solve the allocation problem globally and replace the missing ergodic machinery by a finite-cyclic spectral proof that could be kernel-checked from first principles.

First breakthrough: countably many bad phases

The decisive structural observation is that dyadic abundance makes the set of phases with finite total mass countable.

For a fixed bound on

$$\sum_{n\in A}\|\theta n\|,$$

two sufficiently close phases cannot both satisfy that bound. Indeed, if their difference is δ, look at a dyadic shell at scale about 1/(8δ). Every element of that shell contributes a controlled positive amount to the difference phase, and the growing shell cardinality contradicts the assumed bound. Hence every bounded phase sublevel is finite, and the union of those sublevels is countable.

This converts an uncountable allocation problem into a countable diagonalization. We split off a shell-abundant seed, enumerate only its countably many convergent phases, and balance reserves against those phases. The resulting reserve has syndetic distinct subset sums, while its actual complement still has divergent phase mass for every nonzero phase. Splitting the reserve by rank produces three pairwise-disjoint syndetic finite-sum classes and a disjoint universally phase-divergent correction class.

That resolves the support-allocation obstruction completely.

Second breakthrough: a finite-cyclic proof of the BFW theorem

The remaining input was the Bergelson–Furstenberg–Weiss theorem: the sum of two syndetic subsets of ℕ contains a piecewise-Bohr set.

Instead of formalizing an abstract Kronecker factor, we built the spectral argument from finite cyclic groups.

Dense aligned blocks

A syndetic set has a uniformly positive number of points in long finite blocks. Given dense blocks from two syndetic sets, finite cyclic averaging finds a large fiber on which all pairs have the same exact sum. A dense subblock of that fiber has the property that each positive internal difference, after one common translation, belongs to the original sumset.

Exact spectral measures

For a signal Φ : ZMod N → ℂ, we proved Parseval’s identity for Mathlib’s unnormalized DFT:

$$\sum_k |\widehat\Phi(k)|^2 =N\sum_j|\Phi(j)|^2.$$

Weighting the Nth roots of unity by these squared Fourier magnitudes gives an exact probability spectral measure. Its Fourier coefficients are normalized cyclic autocorrelations, and its mass at the trivial character is the normalized squared mean of the signal.

A cofinal ultrafilter and compactness of probability measures produce a limiting circle measure. Portmanteau’s theorem preserves a positive atom at 1, while positivity of a limiting Fourier coefficient forces the corresponding finite pattern to translate into the syndetic sumset.

Wiener decomposition and piecewise Bohr structure

For an atomless finite circle measure, we formalized Wiener’s lemma directly. The normalized geometric kernel tends to zero off the diagonal, the diagonal has product measure zero, and dominated convergence gives

$$\frac1N\sum_{n<N}|\widehat\mu(n)|^2\longrightarrow0.$$

Every finite measure then splits into:

• a countable atomic Fourier series, uniformly approximable by finitely many characters;
• an atomless remainder with squared-Cesàro-null Fourier coefficients.

The positive atom at 1 makes the finite atomic approximation uniformly positive on a finite-dimensional Bohr neighborhood. The error is smaller than a fixed threshold on a thick set. Their intersection is therefore contained in the Fourier-positivity set.

Finally, compact-rotation return times are syndetic. This lets a smaller pure Bohr neighborhood embed into the piecewise-Bohr set, and the finite-embedding ultrafilter argument transfers it into the original sumset. This yields the full BFW theorem in exactly the finite-torus form required by the number-theoretic argument.

Final assembly

Apply BFW to two of the three disjoint syndetic finite-sum classes. Their sum contains a finite-dimensional piecewise-Bohr return set.

The universally phase-divergent correction class has distinct subset-sum phases dense in the relevant closed torus subgroup. Compactness supplies finitely many corrections that move every large orbit point into the BFW open set. Because all source classes were chosen disjointly in advance, these corrections cannot reuse a base summand. The third syndetic class fills the remaining bounded gaps.

Consequently, every sufficiently large natural number is represented by a finite set of distinct elements of A.

Verification

The formal statement was pinned independently before proof development. The checker byte-compares the canonical statement and root import, rejects every sorry or admit, deletes project build objects, rebuilds the complete dependency graph, kernel-checks the exact theorem type, and audits all transitive axioms.

The accepted command was:

cd /home/azureuser/snapshot && check_answer/verify.sh

Its final output was:

Build completed successfully (8617 jobs).
Erdos254.erdos_254 : Erdos254.Statement
'Erdos254.erdos_254' depends on axioms: [propext, Classical.choice, Quot.sound]
PASS: canonical Erdős 254 statement has a placeholder-free kernel proof

Thus the proof uses only Lean/Mathlib’s standard quotient, extensionality, and classical-choice axioms, with no project-added axiom or proof placeholder.