---

Claim. There is a set $B\subset\mathbb N$ that is not an additive basis, indeed $|B\cap[1,x]|=O((\log x)^6)$, such that for every $0<\alpha<1$, every $A\subseteq\mathbb N$ of Schnirelmann density $\alpha$ and every $N\ge1$ some $b\in B$ satisfies

$$|(A\cup(A+b))\cap\{1,\ldots,N\}|\ge(\alpha+f(\alpha))N,$$

where, with $\beta=1-\alpha$ and $m_0(\alpha)=\lceil16/(\alpha\beta^2)\rceil$, $f(\alpha)=\min\{\beta/2,\ \alpha\beta^2/32,\ 2^{-m_0(\alpha)}\}>0$. This is Theorem 1 of the manuscript "A resolution of Erdős Problem 38" (six pages, PDF metadata dated 25 April 2026, no author named), with the sparsity bound from its abstract and Section 2 (p. 4), and it answers the question yes. The construction discretizes dyadic shift averages by a probabilistic choice of sparse shift multisets and then averages deterministically. The source card states the manuscript's two labeled results and sketches their proofs, in Lemma 1 and Theorem 1.

Claimant. The manuscript names no author. The forum post of 25 April 2026 by the user gebyjaff announces a solution produced by GPT 5.5 Pro, links the shared ChatGPT conversation holding it (the record link above), credits Liam Price with the final cleanup of the PDF, and links the repository holding the PDF, whose single commit is of the same day; the site's commentary credits GPT 5.5 Pro, prompted by gebyjaff.

Acceptance. Thomas Bloom, the site's curator, who is independent of the claimant, accepted the result: the problem page is labeled PROVED (LEAN), was last edited 2 May 2026, and its commentary states, as of 2026-09-05, that a positive solution was given in the comments and that a sparse random set has the property. In the thread, Nat Sothanaphan reported on 26 April 2026 that a standard check of the write-up found no issues, and Bloom posted an alternative sketch of the argument on 2 May 2026, comparing it with Ruzsa's construction of thin essential components. The library pages are this repository's own reading and counts for nothing here. There is no refereed version.

Formalization. The thread links a Lean file (the gist at the pinned revision, posted on 1 May 2026) whose header names Matteo Del Vecchio and Aristotle (Harmonic) as its authors and says it is formalized from the solution by Liam Price and GPT 5.5 Pro; it proves a statement named erdos_problem_38 with the same $f$ and with an asymptotic additive-basis definition. Nat Sothanaphan confirmed that it matches the paper and noted that the asymptotic definition makes the statement stronger. The file was not built or audited here, so it is linked and not counted as formalized. Boris Alexeev's collection lean-proofs holds a modified copy of the gist, Erdos38.lean at the pinned commit, whose header names GPT-5.5 Pro and gebyjaff as the informal authors and Aristotle and Matteo Del Vecchio as the formal authors and cites the forum post and the gist; it is linked above on the same footing and was not built here. The formal-conjectures file that states the problem with a sorry body is described on the problem page; a statement file is not a formalization and is not linked here. The site's (LEAN) suffix is its catalog label, and the community database lists formal_status Lean as of its last update of 1 May 2026 and has no field for a formal proof's location.

Scope. Full. The commentary's stronger quantitative form $f(\alpha)\gg\alpha(1-\alpha)^2$ is not proved in the manuscript and is not part of this claim.