Erdős Problem 347

Reference: erdosproblems.com/347

theorem erdos_347 : (∃ (a : ℕ → ℕ), Monotone a ∧ Filter.Tendsto (fun (n : ℕ) => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 2) ∧ ∀ (ι : ℕ → ℕ), (Set.range ι)ᶜ.Finite → (subsetSums (Set.range (a ∘ ι))).HasDensity 1) ↔ sorry

Is there a sequence $A=\{a_1\leq a_2\leq \cdots\}$ of integers with [\lim \frac{a_{n+1}}{a_n}=2] such that [P(A')= \left{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right}] has density $1$ for every cofinite subsequence $A'$ of $A$?