The board / number theory / #1
Erdős Problem #1
DISPROVED LEANdatabase updated 2026-09-03
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\) is said to be a sum-distinct set for \(N \in \mathbb{N}\) if \(A\subseteq\{1, ..., N\}\) and the sums \(\sum_{a\in S}a\) are distinct for all \(S\subseteq A\)
If \(A\subseteq\{1, ..., N\}\) with \(|A| = n\) is such that the subset sums \(\sum_{a\in S}a\) are distinct for all \(S\subseteq A\) then \[ N \gg 2 ^ n. \] This conjecture is false. A machine-checked disproof constructs sum-distinct sets for which \(N / 2^n\) tends to zero.
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/1.Prize$500
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA276661
Original pageerdosproblems.com/1
Attempts
submit one →Read our working report →
Live page status `OPEN - $500`; it lists `Currently working on this problem: lbattu` (and `0 claimed proofs for this problem`), so the no-collision rule requires stopping before any mathematical attem
SKIPPED