---

Cassels, On the representation of integers as the sums of distinct summands taken from a fixed set, Acta Sci. Math. (Szeged) 21 (1960), 111–124, received 3 September 1959 (the page name's date). Its Theorem II states that for every $\varepsilon>0$ there is a set $C=\{c_1<c_2<\cdots\}$ of positive integers with (i) $(c_{n+1}-c_n)/c_n^{1/2+\varepsilon}\to0$, (ii) infinitely many elements of $C$ in every arithmetic progression, and (iii) $S(n)< \varepsilon n$ for every $n$, where $S(n)$ counts the integers up to $n$ that are sums of distinct elements of $C$. Take $\varepsilon\le1/2$; then condition (i) gives $c_{n+1}/c_n\to1$ (for $\varepsilon>1/2$ it does not); condition (ii) gives every infinite arithmetic progression infinitely many elements of $C$, each a sum of distinct elements of $C$; and condition (iii) leaves the represented integers of upper density at most $\varepsilon$, so infinitely many integers are not represented. The site's remark describes one sequence with gaps $a_i^{1/2+o(1)}$ whose represented integers have density $0$; Theorem II gives, for each fixed $\varepsilon$, gaps $o(c_n^{1/2+\varepsilon})$ and represented integers of upper density at most $\varepsilon$, which is all the disproof needs. The sequence therefore satisfies the hypotheses of Problem 253 and fails its conclusion: the implication is false. The variant of [Va99], which asks only that every infinite progression contain at least one sum of distinct terms, is equivalent, since every tail of an infinite progression is itself an infinite progression, so the same sequence refutes it. The paper's digest is the [[../library/integer_sequences/cassels_1960_representation_integers_as_sums_distinct_summands/_index|library card]], which records Theorem II with its statement checked against the paper; its proof (Section 3) is not reviewed here.

Acceptance. The result is refereed (Acta Scientiarum Mathematicarum), and the site's curator, Thomas Bloom, records the problem as disproved by Cassels with this construction (erdosproblems.com/253, page last edited 23 January 2026, accessed 2026-10-07); the curator had no part in the result. Nothing here is this project's own review.

Formalization. The file src/latest/ErdosProblems/Erdos253.lean of the public repository plby/lean-proofs, linked at the pinned commit of 2026-09-07 (added 2026-08-15; toolchain comment leanprover/lean4:v4.33.0, Mathlib v4.33.0), declares itself a formalization of Cassels's disproof: its header names Cassels as the informal author, the Formal Conjectures authors as the statement authors and Codex and GPT-5.6 Sol as the formal authors, and its docstring describes the witness as a Fibonacci-block version of Cassels's construction. It restates the formal-conjectures statement, RepresentsAPs a saying that $a:\mathbb N\to\mathbb N$ is strictly increasing and that every infinite arithmetic progression meets the set of sums of distinct terms of $a$ in an infinite set, and not_erdos_253 (aliased as erdos_253) proves the negation of the assertion that for every $a$ with $a_0>0$, RepresentsAPs a and $a_{n+1}/a_n\to1$ the sums of distinct terms contain every sufficiently large integer; the file imports only Mathlib and contains no sorry. Registration: the formal-conjectures file 253.lean, linked at the commit of 2026-09-11, carries the attribute formal_proof naming this file at this commit with the category research solved; the community database recorded the problem's formal status as Lean on 2026-08-23; and the site's label carries the Lean suffix (all as of 2026-10-07). The file was neither built nor audited here, so it is linked and not counted as formalized, and its statement's fidelity to the problem is not established by this corpus; the registrations record that a Lean proof exists, not an examination of its statement.