Erdős Problem a Daythe open tracker

Erdős Problem #867

DISPROVED LEANdatabase updated 2026-04-07

The statement as posed is false. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

A finite set of naturals \(A=\{a_1<\cdots<a_t\}\) is *consecutive-sum-free* if it has no solutions to \(a_i+a_{i+1}+\cdots+a_j\in A\) with \(i<j\); equivalently, whenever an interval \([m,n]\) contains at least two elements of \(A\), the sum of the elements of \(A\) lying in \([m,n]\) is not itself an element of \(A\).

Is it true that if \(A=\{a_1<\cdots <a_t\}\subseteq \{1,\ldots,N\}\) has no solutions to \[a_i+a_{i+1}+\cdots+a_j\in A\] then \[\lvert A\rvert \leq \frac{N}{2}+O(1)?\] In fact this problem is false. Freud [Fr93] constructed a sequence with density \(\geq 19/36\). The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an \(A\) satisfies \[\frac{13}{24}N -O(1)\leq \lvert A\rvert \leq \left(\frac{2}{3}-\frac{1}{512}\right)N+\log N.\]
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 5 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/867.
Prizenone
Topicsadditive combinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/867
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.