Problem 741

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive (upper) density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive (upper) density?

Is there a basis $A$ of order $2$ such that if $A=A_1\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?

Source: erdosproblems.com/741

Additive combinatorics

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

Proved; the site labels the problem SOLVED (LEAN), and the suffix is a catalog label explained under Formalization. Both questions are answered yes: the first under the upper-density reading of the Formulation; the second by an explicit basis of order $2$ that no bipartition splits into two self-sumsets with bounded gaps. The claim pages are the DeepMind prover agent's three Lean proofs posted on the site's thread by Moritz Firsching (accepted on the site curator's credit; full), the Alexeev–Putterman–Sawhney–Sellke–Valiant basis from arXiv:2603.29961, attributed by its authors to an internal OpenAI model (accepted on the site curator's credit; partial, the second question only), and a note of April 2026 reproving all three statements (claimed). No refereed publication records any of the answers.

Problem 741

Status

Proof claims

Discussion