---

Fan, Strongly complete sets and a conjecture of Erdős, arXiv:2607.14071, five versions from 15 July 2026 (v1, the page name's date) to 16 September 2026 (v5), held as the library card Fan 2026, which records the versions, the license and the read depth. The paper calls $A\subseteq\mathbb N$ complete if every sufficiently large integer is a sum of distinct elements of $A$, and strongly complete if $A\setminus B$ is complete for every finite $B\subseteq A$; its condition (1.5) is $\sum_{a\in A}\|a\theta\|=\infty$ for every $\theta\in\mathbb R\setminus\mathbb Z$, which is the second hypothesis of Problem 254, since the distance to the nearest integer has period $1$. Corollary 1.2 (p. 4 of v5): every $A$ satisfying (1.5) with $|A\cap(2^k,2^{k+1}]|\ge5$ for every sufficiently large $k$ is strongly complete. The problem's first hypothesis, $|A\cap(x,2x]|\to\infty$, gives at least five elements in every large dyadic interval, so the corollary implies the problem's conclusion and more: the conclusion survives every finite deletion, and Theorem 1.1 (p. 3) at $\rho=2$ gives, when at least $M\ge5$ elements lie in every large dyadic interval, that the number of representations of $n$ as a sum of distinct elements of $A\setminus F$ grows faster than $n^{M-5}$ for every finite $F$. The paper presents the corollary as confirming Erdős's conjecture of 1961 in a strong form.

Theorem 1.1 is proved in Section 4 from a three-component strong-completeness criterion (Theorem 2.2, Section 2) that refines the argument of Bergelson and Simmons. In the base case (pp. 17--18 of v5), where every large interval holds at least $M_\rho$ elements ($M_2=5$), the intervals are split by the parity of their index. One element from each odd-indexed interval forms a sequence with bounded ratios, so the angles at which the distance series over the odd-indexed part converges form a countable set (Lemma 3.1); the deletion lemma (Lemma 3.2) then sets aside $M_\rho-1$ elements of each even-indexed interval while the series over the rest still diverges at each of those angles other than $0$, and the two steps are repeated with the parities exchanged. The set-aside elements are split into two sets $B_1$, $B_2$ whose subset sums have bounded gaps (Lemma 3.3), the kept elements $C$ have a divergent distance series at every nonzero angle and bounded ratios, and the criterion applies to the partition $A=B_1\cup B_2\cup C$. The first version and the proof-claim summary of 16 July 2026 state the threshold as six elements per interval; the current version states five, and the card records Corollary 1.2 and the definitions as unchanged between v4 and v5. The paper's Remark 4.1 (v5) shows that one element per interval does not suffice, so the least threshold lies between two and five; the problem page's Progress section records the corpus's reconstruction of that remark.

Submission note. Posted to erdosproblems.com as a proof claim by Steve Fan (account Steve_Fan) on 16 July 2026, giving "ChatGPT 5.6" as the AI used:

The paper proves general strong-completeness criteria under suitable block-growth and Diophantine conditions. In particular, it is proved that a set $A\subseteq\mathbb{N}$ is strongly complete if $|A\cap(2^k,2^{k+1}]|\ge6$ for sufficiently large $k\in\mathbb{N}$ and

$$\sum_{a\in A}\|a\theta\|=\infty, > \quad\forall\theta\in\mathbb{R}\setminus\mathbb{Z}.$$

This resolves Problem 254

in a strong sense. The proof starts by refining the argument of Bergelson and Simmons to obtain a three-component criterion. Then we select one element from each $(2^k,2^{k+1}]$ to form a sequence $C_0$ with bounded ratios and show that the set of $\theta\in\mathbb{T}\setminus\{0\}$ for which the considered norm series converges is countable. After applying a deletion lemma, we split the reserved elements into two components and adjoining the remaining elements to $C_0$ to produce the desired three-component partition of $A$ which we feed to our new criterion to complete the proof. Notes: The results in the paper are due to the author. Nevertheless, the author used ChatGPT 5.6 to proofread the manuscript before submission. Besides correcting typos, it suggested a core idea underlying the current shorter and more elegant proof of Lemma 3.2 which replaced the author’s original probabilistic argument. All other mathematical ideas and arguments are to be credited or blamed on the author.

Read depth. As the card records: Corollary 1.2, the definitions (1.8)--(1.9) and Remark 4.2 were read clause by clause in the text layer of v5 and compared with v4; Theorem 1.1 and the rest of the paper were read at statement level only, and the proof in Sections 2 to 4 was not read, except the base case of the proof of Theorem 1.1 (pp. 17--18), which was read for its structure.

Formalization. The file src/latest/ErdosProblems/Erdos254.lean of Boris Alexeev's public repository plby/lean-proofs (added 2026-08-26; the formalization link above pins the main head of 2026-09-15, where the file heads a folder Erdos254/ of thirty-one files) declares itself a formalization of this result: its header names Steve Fan, building on Bergelson and Simmons, as the informal author, OpenAI Codex as the formal author, and arXiv:2607.14071v3, Corollary 1.2, as the source. It proves fan_six_per_dyadic, strong completeness for a set with at least six elements in every large dyadic interval $(2^k,2^{k+1}]$ and divergent distance series at every non-integer real angle, the threshold of v1 to v3 rather than the five of v5. It also proves erdos254, the problem's statement with the conclusion written as a finite subset of $A$ summing to each large $n$, through erdos_254_stronglyComplete from the circle-notation form of the same six-per-interval theorem, not from fan_six_per_dyadic, and erdos_254 restates erdos254; comments in the file record the axioms of fan_six_per_dyadic and erdos254 as propext, Classical.choice and Quot.sound.

Acceptance. Formalized. This corpus's verification built Boris Alexeev's repository at the pinned commit of 2026-09-15, in its src/latest project (Lean v4.33.0, Mathlib v4.33.0): the module ErdosProblems.Erdos254 compiled with its imports beside its comparator challenge ComparatorChallenges/ErdosProblems/Erdos254.lean, and the module's files contain no sorry. The axioms of Erdos254.erdos_254 and Erdos254.fan_six_per_dyadic are exactly propext, Classical.choice and Quot.sound. The challenge pins those two theorems with the definitions Erdos254.distToNearestInt, Erdos254.IsSumOfDistinct, Erdos254.IsComplete and Erdos254.IsStronglyComplete, and the fingerprints of both theorems and of the four definitions were found identical to the challenge. The statement was audited clause by clause against the problem's Statement: erdos_254 is at least as strong as the statement as posed. Its set $A$ of natural numbers may contain $0$, which changes nothing; the count difference over $[1,2x]$ and $[1,x]$ is a natural-number subtraction that never truncates, and taking $x$ over the natural numbers only weakens the hypothesis; distToNearestInt sends $x$ to its norm in $\mathbb R/\mathbb Z$, which is the distance from $x$ to the nearest integer, and a nonnegative series that is not summable has infinite sum; and a finite subset of $A$ summing to $n$ gives distinct summands. fan_six_per_dyadic is Fan's six-per-interval criterion of v3: at least six elements in every large dyadic interval and divergence at every non-integer angle give strong completeness. The build is of Alexeev's formalization of v3, with OpenAI Codex as its formal author, not of the v5 preprint: it certifies the statement as posed and the six-per-interval criterion, not the five-per-interval Corollary 1.2 of v5 or the representation counts of Theorem 1.1. Not reviewed: the site's label is OPEN (page last edited 7 December 2025), the tab carries no comment under this claim, and the site's curator, in the thread under the other claim on 16 July 2026, invited the author to post the paper, which is not an acceptance; one forum contributor wrote in that thread on 16 July 2026 that they had read the preprint and found it correct, a thread comment and not a review of record. Not refereed: the paper is a preprint, whose arXiv record carried no journal reference on 2026-10-07. The proof-claim tab lists ChatGPT 5.6 as the AI system used; the paper's AI disclosure (p. 35 of v5) records proofreading assistance and a suggested idea in the proof of Lemma 3.2, the author taking responsibility for the mathematics.

Scope. Full: the claim answers the site's statement, and the corollary gives the stronger conclusion under a weaker hypothesis. The pending claim, Snyder's Lean proof of the statement as posed, is independent of this one; the two share no text and no verification.