Problem 347

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

Source: erdosproblems.com/347

Number theory
Complete sequences

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

Proved, in the site's label "PROVED (LEAN)". Enrique Barschkis posted on 2026-01-21 an explicit block construction, from an idea of Tao and van Doorn, with a Lean proof; a named reader, working with ChatGPT, checked both, and the site accepted the result (page last edited 22 January 2026, accessed 2026-10-07). See the claim page (Barschkis, 2026). The "(LEAN)" suffix is the site's label: nothing was built or audited here.

Problem 347

Status

Proof claims

Discussion