Problem #350: If $A\subset\mathbb{N}$ is a finite set of integers which...

---

Progress

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\}$.

The stronger statement that, for all $s\geq 0$,\[\sum_{n\in A}\frac{1}{n^s} <\frac{1}{1-2^{-s}},\]was proved by Hanson, Steele, and Stenger [HSS77].

See also [1].

This problem has been formalised in Lean as part of the Google DeepMind Formal Conjectures project.