The board / number theory / #771
Erdős Problem #771
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`IsAdmissible n k` says that for every \(m \geq 1\) there is a \(k\)-element \(S \subseteq \{1,\ldots,n\}\) such that no subset of \(S\) sums to \(m\).
\(f(n)\): the largest \(k\) such that for every \(m \geq 1\) there is a \(k\)-element \(S \subseteq \{1,\ldots,n\}\) with \(m \neq \sum_{a \in A} a\) for all \(A \subseteq S\). The set of such \(k\) contains \(0\) and is bounded by \(n\), so `sSup` is its maximum.
Let \(f(n)\) be maximal such that, for every \(m\geq 1\), there exists some \(S\subseteq \{1,\ldots,n\}\) with \(\lvert S\rvert=f(n)\) such that \(m\neq \sum_{a\in A}a\) for all \(A\subseteq S\). Is it true that \[f(n) = \left(\frac{1}{2}+o(1)\right)\frac{n}{\log n}?\] The answer is yes: the lower bound is due to Erdős and Graham and the upper bound to Alon and Freiman [AlFr88].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/771.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/771
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.