The board / number theory / #350
Erdős Problem #350
PROVED LEANdatabase updated 2025-11-25
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).
The predicate that all (finite) subsets of `A` have distinct sums.
The predicate that all (finite) subsets of `A` have distinct sums, decidable version
If `A ⊂ ℕ` is a finite set of integers all of whose subset sums are distinct then `∑ n ∈ A, 1/n < 2`. Proved by Ryavec. This was proved by Ryavec, who did not appear to ever publish the proof. Ryavec's proof is reproduced in [BeEr74]. More generally, Ryavec's proof delivers that \(\sum_{n\in A}\frac{1}{n}\leq 2-2^{1-\lvert A\rvert},\) with equality if and only if \(A=\{1,2,\ldots,2^k\}\). This was formalized in Lean by Alexeev using Aristotle.
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/350.Prizenone
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/350
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.