---

Claim. On 2026-01-21 Enrique Barschkis (forum name ebarschkis) posted in the thread of Problem 347 a note, its source and a Lean proof answering the question yes: there is a nondecreasing sequence $A$ of positive integers with $a_{n+1}/a_n\to2$ such that, for every cofinite subsequence $A'$, the set $P(A')$ of finite subset sums has asymptotic density $1$. The sequence follows a block sketch that Terence Tao posted in the thread on 2025-10-25, itself a variant of an idea that Wouter van Doorn (forum name Woett) had posted there the same day; Barschkis's post says it is based on the ideas of Tao and Woett. Block $n$ consists of $M_n,2M_n,\ldots,2^{k_n-2}M_n$ followed by $(2^{k_n-1}-1)M_n+1$, with block lengths $k_n$ growing slowly (about $\log_2\log_2n$) and scales $M_{n+1}\approx(2^{k_n}-1.5)M_n$, so that consecutive ratios tend to $2$. For a cofinite $A'$ the tail blocks give a base-like greedy representation of almost every integer, and the shifted last term of each block supplies the carries, leaving a set of exceptions of density zero. The site's commentary credits the affirmative solution to ebarschkis in the thread, building on the idea of Tao and van Doorn posted there.

Formalization. The posted Formalization.lean (Lean 4.24.0 with the Mathlib revision named in its header; generated by Aristotle, Harmonic's automated prover, according to that header) ends with answer_is_yes: there is a monotone $A:\mathbb{N}\to\mathbb{N}$ whose consecutive ratios tend to $2$ such that every $S\subseteq\operatorname{range}A$ with finite complement has subset sums of asymptotic density one. Barschkis wrote in the thread on 2026-01-21 that they used GPT Codex to write the note's LaTeX and improve parts of it and had much help from Bartosz Naskrecki; van Doorn's file header says Naskrecki helped Barschkis obtain the Lean formalization with Aristotle. Van Doorn posted the same day a trimmed version that removes native_decide and reports through #print axioms only propext, Classical.choice and Quot.sound: they committed it to their repository on 2026-01-21, then named ErdosProblem#347.lean, and linked from the thread a live.lean-lang.org check that loads that file; on 2026-03-02 they renamed it to the pinned path, that path's only commit, with the file's contents unchanged. The formal-conjectures statement erdos_347 (category research solved) points to the posted proof through its formal_proof attribute and is itself sorry; it is a statement file, listed as a record, not a formalization. Nothing was built here and the fidelity of the Lean statement to the problem's wording was not audited, so no formalized evidence is listed; the problem page's "(LEAN)" suffix is the site's label.

Acceptance. Reviewed: Nat Sothanaphan reported in the thread on 2026-01-22, from an assessment made with ChatGPT as their post states, that the Lean proof compiles and proves the right statement, that it corresponds to the informal note, and that the note is correct apart from omitted details they list; Tao wrote on 2026-01-21 that the handling of the slowly growing block length looks plausible; the site's curator, T. F. Bloom, labels Problem 347 PROVED (LEAN) at erdosproblems.com and credits the result to Barschkis (page last edited 22 January 2026, accessed 2026-10-07), and the community database lists the problem as proved (Lean), its entry last updated on 2026-01-21. A later thread comment (2026-02-04) describes a parametric generalization of the construction in Lean; it is not part of this claim. Nothing here was checked by this project.