Erdős problem 350

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.