Erdős Problem #355

Is there a lacunary sequence \(A\subseteq \mathbb{N}\) (so that \(A=\{a_1 < \cdots\}\) and there exists some \(\lambda > 1\) such that \(a_{n+1}/a_n\geq \lambda\) for all \(n\geq 1\)) such that \[\left\{ \sum_{a\in A'}\frac{1}{a} : A'\subseteq A\textrm{ finite}\right\}\] contain all rationals in some open interval? Bleicher and Erdős conjectured the answer is no. In fact the answer is yes, with any lacunarity constant \(\lambda\in (1,2)\) (though not \(\lambda=2\)), as proved by van Doorn and Kova\v{c} [DoKo25]. This was formalized in Lean by van Doorn using Aristotle.