PROVED (LEAN)
This has been solved in the affirmative and the proof verified in Lean.
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$?
