---

Submitted to the proof-claim tab of Problem 254 on 15 July 2026 by Colin Snyder as a full proof claim produced with GPT 5.6 in a custom harness, as the tab names the system. The claim is the statement as posed: if $|A\cap[1,2x]|-|A\cap[1,x]|\to\infty$ and $\sum_{n\in A}\|\theta n\|=\infty$ for every $\theta\in(0,1)$, then every sufficiently large integer is a sum of distinct elements of $A$, proved in Lean 4 with Mathlib as Erdos254.erdos_254 : Erdos254.Statement, with the axiom list propext, Classical.choice, Quot.sound and no placeholder, according to the submission and the hosted write-up. The argument, as the write-up describes it: dyadic growth makes the set of angles at which the distance series converges countable: for each bound, two distinct angles close enough together cannot both have mass below it (if they differ by $\delta$, each element of a dyadic shell at scale about $1/(8\delta)$ contributes a fixed positive amount at the difference angle, and the shells grow), so each sublevel set is finite; a countable diagonalization then splits $A$ into three disjoint classes whose sets of distinct subset sums are syndetic and a disjoint correction class on which every nonzero angle still diverges; the theorem of Bergelson, Furstenberg and Weiss, that the sum of two syndetic sets contains a piecewise Bohr set, is proved in the bundle from finite cyclic Fourier analysis (Parseval's identity for the discrete Fourier transform on cyclic groups, spectral measures, ultrafilter limits and Wiener's lemma) instead of from a Kronecker factor; the correction class is used to shift any large integer into that Bohr set, the third class covers the bounded gaps that remain, and the summands are distinct because the classes are disjoint.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

We claim a complete proof of the statement as posed: if $|A\cap[1,2x]|-|A\cap[1,x]|\to\infty$ and $\sum_{n\in A}|\theta n|=\infty$ for every $\theta\in(0,1)$, then every sufficiently large integer is a sum of distinct elements of $A$. Proved in Lean 4 / Mathlib (theorem Erdos254.erdos_254), standard axioms only, no sorry. Idea: dyadic growth forces the set of phases with finite mass to be countable, which lets us split $A$ into three disjoint syndetic classes with distinct subset sums plus a correction class that keeps every phase divergent. By Bergelson-Furstenberg-Weiss, the sum of two syndetic classes contains a piecewise-Bohr set; the correction class steers every large integer into it, and the third class fills the remaining bounded gaps. Disjointness keeps all summands distinct. Notes: The piecewise-Bohr sumset theorem is due to Bergelson, Furstenberg and Weiss; since it is not in Mathlib, the bundle includes a new fully finite/cyclic proof of it (exact cyclic Parseval, a formalised Wiener lemma, ultrafilter limits) suitable for kernel checking. Verify: run check_answer/verify.sh (pins the statement, rejects sorry/admit, rebuilds ~8,600 jobs); the axiom line is exactly [propext, Classical.choice, Quot.sound].

The bundle. The downloadable archive (124,569 bytes; its entries are dated 11 to 13 July 2026) holds a Lean project of fifty-eight files under Research/, a checker script, and a record entry dated 11 July 2026. Its check_answer/Statement.lean defines the distance to the nearest integer as $\min(\{x\},1-\{x\})$ with $\{x\}$ the fractional part, the count of members of $A$ in $[1,x]$ over the finite interval of integers, the dyadic increment as the difference of the counts at $2x$ and $x$, the partial sums of the distances over $A\cap[1,N]$, completeness as a threshold beyond which every integer is the sum of a finite set contained in $A$, and Statement as: for every $A\subseteq\mathbb N$, if the dyadic increment tends to infinity along integer cutoffs and for every $\theta\in(0,1)$ the partial sums tend to infinity, then $A$ is complete. That file matches the site's wording in the integer-cutoff reading; the equivalence with a real cutoff is the bundle's own argument and is not examined on this page. The checker byte-compares the statement, rejects placeholders, rebuilds the project and prints the axioms; the hosted page reports the run's output (8,617 jobs and the axiom line) and an unsigned section headed "Independent referee", written in the first person on the hosting platform and naming no outside reviewer, whose author compared the statement with the formal-conjectures encoding and rebuilt the project. That section is a statement on the hosting platform, not an outside review. The corpus has not built, kernel-checked or audited the development.

Standing. Claimed: the site's label is OPEN (page last edited 7 December 2025; proof-claims tab read 2026-10-07), the eight comments under the claim (16 to 18 July 2026) concern Fan's preprint, posted to arXiv later that day and to the proof-claim tab on 16 July, and none assesses this proof. Since 2026-08-07 formal-conjectures marks its statement erdos_254 research solved with a formal_proof pointer to this development: the file starfleet/erdos-254/Research/Basic.lean of the williamjblair/lean-proofs repository, at the commit of 2026-07-30 pinned by the second formalization link above, which is the same Star Fleet Math project as the bundle (its Research/ folder and its check_answer/verify.sh). That is a catalog registration, not a review. No refereed version, site acceptance or independent review is recorded, and the corpus has neither built nor audited the development, so there is no formalized evidence.

Scope. Full: the claim answers the site's statement. Fan's independent preprint, accepted on a Lean formalization of its six-per-interval version, proves the stronger conclusion of strong completeness under the weaker hypothesis of five elements per dyadic interval; this claim proves the statement as posed and nothing beyond it.