---

Claim. The answer to Problem 867 is no: a set $A\subseteq\{1,\ldots,N\}$ in which no member is a sum of two or more consecutive members can have $\tfrac{19}{36}N-O(1)$ members, so no bound $\lvert A\rvert\le N/2+O(1)$ holds. The claimed result is the construction of R. Freud, Adding numbers, a note in the James Cook Mathematical Notes (1993): for positive integers $x,y$ with $x=17y-2$, four blocks, the $4y+1$ consecutive integers around $2x$, the $4y$ integers around $3x$ not divisible by $3$, the $4y-1$ even integers around $4x$, and all integers from $4x+4y+2$ to $8x+8y+4$, with the $8y+2$ members of the last block that are sums of consecutive members deleted, form a set of $76y-7$ integers up to $N=144y-12$ with the required property, so that

$$\lvert A\rvert=\frac{19}{36}N-\frac23 \quad\text{and}\quad \lvert A\rvert-\frac N2=\frac N{36}-\frac23\to\infty$$

along these $N$; for every $N\ge144$ the set built for the largest $144y-12\le N$ still has $\tfrac{19}{36}N-O(1)$ members. Repeating the construction with rapidly growing parameters gives an infinite sequence with $\limsup A(n)/n=\tfrac{19}{36}$, which also answers Erdős's remark that the upper density of such a sequence probably cannot exceed $\tfrac12$. The construction, the deletion count and the two totals are recomputed here, as the result page records; the verification that no remaining member is a consecutive sum is Freud's and is not independently checked. The note is a contribution to a mathematical notes bulletin and is not described as refereed.

Depends on. Nothing in this wiki.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem disproved and credits Freud [Fr93] with a sequence of density at least $\tfrac{19}{36}$ (on 2026-09-18 and 2026-10-07; the proof-claim tab is empty), after a thread comment of 2025-09-02 reported the note and the Coppersmith--Phillips paper as a negative solution; and D. Coppersmith and S. Phillips, in a refereed paper (SIAM J. Discrete Math. 9 (1996), 173--177), cite the note as their reference [1] and open the proof of their Theorem 2.1 from Freud's construction, which Freud's note in turn reports they had rediscovered and improved. Their improvement is recorded on its own claim page. Not refereed: the note itself carries no refereeing record. The page is dated to the January 1993 issue (issue 60, printed pp. 6199--6202), filled to the first of the month. The paper link above is the bulletin's scan of the whole issue, hosted on the James Cook Mathematical Notes site, which carries the note on printed pp. 6199--6202; the thread comment of 2025-09-02 links the same scan.

Formalization. Not counted as evidence: on 2026-04-07 Pietro Monticone posted to the site's thread that the solution had been autoformalized with the prover Aristotle, linking a Lean 4 file in a gist. The file, imported into Boris Alexeev's lean-proofs repository on 2026-05-07 (pinned above at the repository's commit of 2026-09-15; its header names Freud as informal author and Aristotle and Monticone as formal authors), defines consecutive-sum-freeness over contiguous sublists of the sorted members, builds Freud's four blocks as freudSet y, proves their count $76y-7$, their containment in $\{1,\ldots,144y-12\}$ and their freeness for $y\ge1$, and derives construction_19_36 (a set of at least $(19n-2741)/36$ members for every $n\ge144$) and csf_exceeds_half_plus_constant, the negation of the bound $2\lvert A\rvert\le n+C$ for a natural constant; it contains no sorry and no axiom declaration, and its closing comments record #print axioms for both theorems as propext, Classical.choice and Quot.sound. The formal-conjectures statement file, whose own theorem is sorry and whose ConsecutiveSumFree is defined over intervals with a real constant, names the repository's file on its main branch as the formal proof; no bridging declaration exists in either file. The corpus holds no build of the file, so it gives no formalized evidence; the community database records the problem as "disproved (Lean)", with a last update for the problem dated 2026-04-07 that does not date the change of state. The problem's standing rests on the construction as the site and the refereed paper accept it.