Erdős Problem #347

Full solution by Enrique Barschkis, Wouter van Doorn, jbbaehr22, Bartosz Naskrecki and Terence Tao with Aristotle, Claude Opus, Codex and GPT, formalized in Lean (25 Oct 2025).

Problem
Erdős problem #347 (number theory, complete sequences); current status: proved (Lean)
Credit
Enrique Barschkis, Wouter van Doorn, jbbaehr22, Bartosz Naskrecki and Terence Tao with Aristotle, Claude Opus, Codex and GPT · AI working with humans
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2025-10-25 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
SOLVEDPer Tao's AI-contributions wiki

The problem

Is there a sequence A={a1≤a2≤⋯ }A=\{a_1\leq a_2\leq \cdots\} of integers with

lim⁡an+1an=2\lim \frac{a_{n+1}}{a_n}=2

such that

P(A′)={∑n∈Bn:B⊆A′ finite }P(A')= \left\{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right\}

has density 11 for every cofinite subsequence A′A' of AA?

Statement quoted from erdosproblems.com/347, maintained by Thomas Bloom. Original source: [ErGr80]. Current status there: proved (Lean).

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Humans Outcome
25 Oct, 2025-4 Feb, 2026 AI working with humans Aristotle, Claude Opus, Codex, GPT Enrique Barschkis, Wouter van Doorn, jbbaehr22, Bartosz Naskrecki, Terence Tao 🟢 Full solution (Lean)
25 Oct, 2025 Literature search ChatGPT Deep research — 🟡 Partial results found

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎