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?

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č [DoKo25].

This was formalized in Lean by van Doorn using Aristotle.