---

Claim. The note A note on Erdős problem 741, dated 23 April 2026 and carrying no author line, states and proves three theorems about Problem 741: if $\overline d(A+A)>0$ then $A=A_1\sqcup A_2$ with $\overline d(A_1+A_1)>0$ and $\overline d(A_2+A_2)>0$ (Theorem 1.2); there is $A$ with $d(A+A)=1$ such that no partition gives both $d(A_1+A_1)$ and $d(A_2+A_2)$ existing and positive (Theorem 1.3); and there is an asymptotic basis $A$ of order $2$ such that for every partition one of $A_1+A_1$, $A_2+A_2$ is not syndetic (Theorem 1.4). Its introduction says the aim is to package the results already on the site's thread and in the Alexeev–Putterman– Sawhney–Sellke–Valiant preprint into one self-contained note and to compare the two bases. Przemek Chojecki posted it on the thread on 2026-04-24, writing that they had GPT-5.4 Pro produce the note and Aristotle formalize it; the Lean file at the same host states the three theorems (erdos741_upper_density, erdos741_strict_density_counterexample, erdos741_syndetic) over Mathlib with its own BiPartition, IsAsympBasisOrder2 and IsSyndetic' and contains no sorry or axiom declaration and no recorded #print axioms output. This project has not verified the note's proofs. The note reproves the results of the DeepMind claim page and of the Alexeev–Putterman–Sawhney–Sellke–Valiant claim page rather than building on them.

Submission note. Posted to the site's forum by Przemek Chojecki on 24 April 2026:

What is missing here to mark this problem as solved? Looks like the first question is false for strict natural density, but true for upper density; the second question has an affirmative answer.

I've run GPT-5.4 Pro to have a full note proving all these results plus compare to DeepMind/OpenAI constructions. Here's the note and here's a full formalization of it with Aristotle.

Depends on. Nothing in this wiki.

Standing. Claimed. The note is hosted on the submitter's own site, is not on arXiv and not refereed, and the site's curator neither replied to the post nor credits it in the problem page's commentary (page last edited 2 May 2026); this corpus has not built the Lean file, and no outside reviewer has published an examination. The problem's standing rests on the accepted claims above.