---

Claim. There is a set $A\subset\mathbb{N}$ of positive upper density that is a minimal asymptotic basis of order two: every sufficiently large integer is a sum of two elements of $A$, and for every $a\in A$ the set of integers that are not a sum of two elements of $A\setminus\{a\}$ has positive upper density, so no element can be removed. This answers the question of Erdős and Nathanson yes, with the "positive density" of $A$ read as positive upper density, the reading the site says Erdős most likely intended, and with the integers that need an element measured by upper density, as the statement says. The construction was posted to the site's thread on 2026-04-24 by the forum user DavidTurturean, who writes that an automated audit-and-revise scaffold of their own queried ChatGPT-5.5-Pro for about fifteen turns on the model's release day; the write-up is the linked Overleaf document, and the site credits the construction to the model as prompted by Turturean. A thread participant's reconstruction of the argument (comment of 2026-04-25), which they flagged as possibly inexact since they found the exposition hard to follow and worked it out themselves, assigns to each element a large prime so that the integers needing that element as a summand contain long arithmetic progressions, reusing the primes across iterations while keeping positive upper density.

Depends on. No page of this wiki.

Acceptance. Reviewed: the site's curator, T. F. Bloom, relabeled Problem 330 proved at erdosproblems.com (its page last edited 2026-05-11), crediting the construction to GPT 5.5 Pro, the site's spelling, as prompted by Turturean; this is the site's acceptance and the only review listed. The claimant's post linked two ChatGPT-5.5-Pro transcripts checking the write-up, and on the thread a thread participant posted that a standard check found no issues (2026-04-24) and later that the Lean development is correct and largely matches the proof (2026-05-05), each post linking a ChatGPT transcript; these are AI checks and add no independent review. A thread comment of 2026-05-01 posted an AI reading of the write-up which found it under-attributed to the minimal-basis literature (Erdős–Nathanson, Jańczak–Schoen) but no prior proof of the theorem, and which the poster flagged as not a real critique. There is no refereed publication.

Two Lean developments formalize the claim. The first, announced on the thread on 2026-05-05 and pinned at its folder's commit of 2026-05-10, is a 21-module development planned with ChatGPT 5.5 Pro and written with Codex under human supervision, as its author's post names them; its target MainTarget states a set that is an asymptotic basis of order two with positive upper density whose private sets all have positive upper density, with upper density as the limit superior of the partial densities. The second, a single-file vendoring of that development at a commit of 2026-08-06, is the proof that the formal-conjectures statement file links for its erdos_330_statement, tagged research solved; the formal-conjectures statement itself quantifies existentially over the order and stays sorry. Neither development has been built or audited in this corpus, so formalized is not listed and the Lean qualification of the site's label is the site's.