この記事の日本語版はまだありません。英語版を表示しています。

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).

問題
Erdős problem #347 (number theory, complete sequences); current status: proved (Lean)
貢献
Enrique Barschkis, Wouter van Doorn, jbbaehr22, Bartosz Naskrecki and Terence Tao with Aristotle, Claude Opus, Codex and GPT · AI working with humans
検証
Lean formalizationListed in Tao's wiki
経緯
First AI contribution 2025-10-25 · wiki data as of 2026-06-30
出典
Problem page (erdosproblems.com)Tao's AI-contributions wiki
完全解Per 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.

∎