Erdős Problem 347

Reference: erdosproblems.com/347

theorem Erdos347.erdos_347 : True ↔ ∃ (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

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$?

This has been solved in the affirmative by ebarschkis in the comments (based on idea of Tao and van Doorn, also in the comments).

Thos was formalized in Lean by Barschkis using Aristotle.