The board / number theory / #362
Erdős Problem #362
PROVED LEANdatabase updated 2026-08-24
The statement as posed is true, and a proof exists. 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).
Let \(A\subseteq \mathbb{N}\) be a finite set of size \(N\). Is it true that, for any fixed \(t\), there are \[\ll \frac{2^N}{N^{3/2}}\] many \(S\subseteq A\) such that \(\sum_{n\in S}n=t\)? Erdős and Moser [Er65] proved the first bound with an additional factor of \((\log n)^{3/2}\). This was removed by Sárközy and Szemerédi [SaSz65], thereby answering the first question in the affirmative. Stanley [St80] has shown that this quantity is maximised when \(A=\{-\lfloor \frac{N-1}{2}\rfloor,\ldots,\lfloor\frac{N}{2}\rfloor\}\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/362.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/362
Attempts
submit one →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.