---

Claim. Every set $A$ of $n$ integers has a sum-free subset $B$, one in which no element is the sum of two or more other distinct elements of $B$, with

$$|B|\gg\frac{n}{(\log n)^2},$$

so that $l(n)\gg n/(\log n)^2$ in the notation of Problem 790. This proves the conjecture of Choi, Komlós and Szemerédi that $l(n)\ge n^{1-o(1)}$ and, with their upper bound $l(n)\ll n/\log n$, places $l(n)$ within a factor of $\log n$: the first displayed question keeps its affirmative answer, and the second is answered in the negative, since $l(n)<n^{1-c}$ then fails for every $c>0$ and all large $n$. The route, as the claim's summary describes it: where the 1975 proof passes to subsequences whose gaps are monotone, the claim instead halves repeatedly and gives each element $O(\log n)$ distances, chosen so that every pairwise difference lies within a factor of two of a distance at one of its two endpoints; in an additive relation the difference of the two largest terms lies between the third-largest term and $n$ times it, so each point has only $O((\log n)^2)$ dyadic intervals to avoid; a random choice of intervals, keeping the points that fit them, leaves a sum-free subset of the expected size. The claim was submitted on 2026-09-13 by Samuel Korsky, the author of a preprint on progression-free subset sums for Problem 817 (source card), and declares the use of GPT Astra. The claimant's own note leaves it to taste whether the result is a full resolution, since a factor of $\log n$ remains between the bounds; the tab files it as a full claim, and this page records that scope. The write-up is a document on a file-sharing service, linked above.

Submission note. Posted to erdosproblems.com as a proof claim by Samuel Korsky (account SamKorsky) on 13 September 2026, giving "GPT Astra" as the AI used:

We show that

$$l(n)\gg n/(\log n)^2,$$

proving the Choi–Komlós–Szemerédi

conjecture that $l(n)\ge n^{1-o(1)}$. The idea is to replace the extraction of subsequences with monotone gaps in [CKS75] by a repeated-halving construction. This associates $O(\log n)$ distances with every original element, so that every pairwise difference is approximated within a factor of two by a distance associated with one endpoint. An additive relation forces the difference between its two largest terms to lie between its third-largest term and $n$ times that term. The distance lists therefore identify only $O(\log^2 n)$ dyadic intervals that each point must avoid. Randomly selecting intervals and retaining compatible points gives a sum-free subset of expected size. Notes: I submitted this as a full proof claim because it answers both specific questions about $l(n)$ and shows that the correct exponent is $1$, but as with #789 it is up to personal taste whether this counts as a full resolution as there is still a logarithmic gap between the known lower and upper bounds.

Depends on. Choi, Komlós and Szemerédi's theorem, whose upper bound the completeness statement uses and whose lower-bound method the claim modifies.

Standing. Claimed. The site's label was OPEN on 2026-09-18 and on 2026-10-06 and its commentary does not mention the claim; no arXiv version, refereed publication or independent review was found on 2026-09-18. The claim thread carries two comments: a reader's favorable remark of 2026-09-14, which is not a review, and an announcement of 2026-10-05 of a third-party Lean 4 formalization of the claim, linked above at its pinned commit, which defines $l(n)$ literally and proves $l(n)\ge cn/(\log n)^2$, both displayed questions and $\log l(n)/\log n\to1$. Its two authors present it as a formalization of the claimant's proof, the mathematics being entirely theirs apart from replacing a random choice of dyadic intervals by an exact weighted average, state that it was produced with the assistance of Claude (Anthropic), and report it sorry-free with only the standard axioms propext, Classical.choice and Quot.sound. Being a formalization of a named claimant's result, it is a link on this page and not a claim of its own; this corpus has not built or audited the development, so no formalized evidence is listed and the standing stays claimed. The lower bound in force on the problem page is the 1975 theorem's $(n\log n/\log\log n)^{1/2}$.