A density and equidistribution condition forcing subset-sum completeness (Erdős #254)
Statement
For a real $x$ write $\lVert x\rVert$ for the distance from $x$ to the nearest integer. Suppose $A\subseteq\mathbb{N}$ satisfies both a dyadic growth condition $$\lvert A\cap[1,2x]\rvert-\lvert A\cap[1,x]\rvert\to\infty\quad(x\to\infty)$$ and an equidistribution condition $$\sum_{n\in A}\lVert\theta n\rVert=\infty\quad\text{for every }\theta\in(0,1).$$ Prove that then every sufficiently large integer is a sum of distinct elements of $A$ (i.e. $A$ is 'complete').
Acceptance. FULLY RESOLVES: prove that any $A\subseteq\mathbb{N}$ satisfying Erdős's two hypotheses is complete (every sufficiently large integer is a sum of distinct elements of $A$), with a complete proof — Lean/Coq preferred, else a full written proof. ADVANCES (each checkable): prove completeness under hypotheses strictly weaker than Cassels's stated in the background (for instance replacing the $\lVert\theta n\rVert^2$ series by $\lVert\theta n\rVert^{2-\delta}$, or weakening the $\log\log x$ counting requirement), delivering a proof that names exactly which hypotheses are used and how they improve on Cassels; or exhibit a counterexample — a fully specified $A$ satisfying Erdős's hypotheses together with a proof that arbitrarily large integers are not sums of distinct elements of $A$ — which would disprove the conjecture. Deliver the proof file, or the explicit counterexample sequence with its non-representability proof.
Background
Asked by Erdős [Er61]. Listed as open on erdosproblems.com/254 (fetched 2026-07-13, status 'open', tagged 'number theory'); a Lean 4 formalisation exists in google-deepmind/formal-conjectures. The problem proposes a candidate sufficient condition for a sequence to be COMPLETE (every large integer expressible as a sum of distinct terms). The two hypotheses are natural: the counting condition forces $A$ to be reasonably dense on every dyadic scale, while $\sum_{n\in A}\lVert\theta n\rVert=\infty$ prevents $A$ from clustering near an arithmetic structure (a lacunary or geometric-like set whose subset sums avoid residue classes). Best known: Cassels [Ca60] proved completeness under STRONGER hypotheses — that $\big(\lvert A\cap[1,2x]\rvert-\lvert A\cap[1,x]\rvert\big)/\log\log x\to\infty$ and $\sum_{n\in A}\lVert\theta n\rVert^2=\infty$ for every $\theta\in(0,1)$ (the squared series is more restrictive than Erdős's). Closing the gap between Cassels's hypotheses and Erdős's weaker ones is the open problem. Compare the venue's Burr–Erdős–Graham–Li completeness conjecture (Erdős #124, erdosproblems.com/124). No Erdős prize is recorded. Attacker's tool: the Fourier / circle-method machinery behind Cassels-type completeness theorems (bounding the exponential sum $\sum_{n\in A} e(\theta n)$ using the given $\lVert\theta n\rVert$ series and combining with the dyadic counting hypothesis), targeting a Lean formalisation; the claim is universal over all admissible $A$, so computation can only test, not prove it.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #254 (T. F. Bloom) | website |
| REF-02 | Lean 4 formalisation — google-deepmind/formal-conjectures #254 | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.