theorem Erdos355.erdos_355 : (∃ (A : ℕ → ℕ), IsLacunary A ∧ ∃ (u : ℝ) (v : ℝ), u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x : ℚ | ∃ (A' : Finset ℕ) (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}) ↔ sorry

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?