---

Claim. The answer to Problem 333 is no. A post to the problem's forum thread on 2025-12-25 gave a direct construction of a set $A\subseteq\mathbb{N}$ of density zero such that no $B\subseteq\mathbb{N}$ with $A\subseteq B+B$ has $\lvert B\cap\{0,\ldots,N\}\rvert=o(N^{1/2})$, by a greedy hitting-set argument over dyadic blocks: in each block a finite set of hard-to-cover integers is chosen so that any $B$ representing all of it as sums of two elements has at least a constant times the square root of the block's size of its elements below the block's end, and the pieces are thin enough that their union has density zero. The post attributes the argument to the AI system GPT-5.2 Pro and its formalization to Claude Opus 4.5; the Lean file names Erdős, Newman and GPT-5.2 Pro as its informal authors and Claude Opus 4.5, Liam Price and Kevin Barreto as its formal authors. The forum post is Barreto's, who writes that their only role was to ask GPT-5.2 Pro for the construction, so the page is named for Barreto as the claim's submitter.

Submission note. Posted to the site's forum by Kevin Barreto on 25 December 2025:

Interpreting the problem in the way suggested by Woett: "Let $A\subseteq \mathbb{N}_0$ be a set of natural density zero. Does there exist a basis $B$ for $A$ such that $A\subseteq B+B$ and

$$\lvert B\cap \{0,\ldots,N\}\rvert > =o(N^{1/2})$$

for all large $N$?"

GPT-5.2 Pro provides a negative answer to this here (and with conventions elaborated on here). We believe, to the best of our knowledge, this is the first case of an LLM fully autonomously resolving an Erdős problem, not previously resolved by humans. GPT-5.2 Pro's solution was then autoformalised in Lean 4 by Claude Opus 4.5, and is viewable here. There was no human input to the argument of the proof. Originally, GPT-5.2 gave a probabilistic argument which appeared correct but annoying to formalise; my only role was in asking GPT-5.2 Pro to give a more constructive argument and instructing Claude Opus 4.5 to search through the Mathlib4 GitHub repository for relevant tactics as it formalised GPT-5.2 Pro's informal proof. Everything else was end-to-end.

We sketch the argument given by GPT-5.2 Pro here. We prove that there exists a set $A\subseteq\mathbb{N}_0$ of density zero such that there does not exist a set $B\subseteq\mathbb{N}_0$ with $A\subseteq B+B$ and $\left|B\cap[0,N]\right|=o(\sqrt{N})$.

$\textit{Proof sketch.}$ Fix $\varepsilon=\frac{1}{10}$. For a dyadic $N=2^n$, with $n\geq 3$, we construct a finite set

$$> A_N\subseteq J_N:=\left\{\frac{N}{2}+1,\,\frac{N}{2}+2,\,\dots,\,N\right\}, >$$

with $|J_N|=\frac{N}{2}$. Then, we define

$$> A:=\bigcup_{n\geq 3}A_{2^n}. >$$

Because the intervals $J_{2^n}\subset (2^{n-1},2^n]$ are disjoint, $A$ is a disjoint union of blocks. Now let

$$> m:=\left\lfloor\varepsilon\sqrt{N}\right\rfloor,\qquad\mathcal{B}_N:=\{B\subseteq[0,N]:\left|B\right|\leq m\}. >$$

We want $A_N\subseteq J_N$ such that $\forall B\in\mathcal{B}_N,
A_N\not\subseteq B+B$. For $B\in\mathcal{B}_N$, let

$$> S_B:=(B+B)\cap J_N,\qquad C_B:=J_N\setminus S_B. >$$

Then, we have the trivial bound $\left|B+B\right|\leq\left|B\right|^2\leq m^2\leq\varepsilon^2 N$. Hence,

$$> \left|S_B\right|\leq\varepsilon^2 N,\qquad\left|C_B\right|\geq\left|J_N\right|-\varepsilon^2 N=\frac{N}{2}-\varepsilon^2 N. >$$

So, each $C_B$ occupies a fixed positive fraction of $J_N$ (for $\varepsilon=1/10$, it is $\geq 0.49N$). We then apply a greedy hitting-set lemma:

$\textit{Lemma}$ (Greedy hitting-set). If a finite family of subsets of a universe $U$ each has size $\delta\left|U\right|$, then there is a set $H\subseteq U$ meeting every member, with $\left|H\right|\ll_{\delta}\log\left|\mathcal{F}\right|$.

Here, $U=J_N$ and $\mathcal{F}=\{C_B:B\in\mathcal{B}_N\}$. Since each $C_B$ is a fixed-density subset of $J_N$, we obtain $A_N\subseteq J_N$ such that

$$> A_N\cap C_B\neq\varnothing\qquad\forall B\in\mathcal{B}_N, >$$

which is exactly the desired property $A_N\not\subseteq B+B$. We have the folloowing size control: $\left|A_N\right|\ll\log\left|\mathcal{B}_N\right|$, and

$$> \left|\mathcal{B}_N\right|=\sum_{i\leq m}\binom{N+1}{i}\leq(m+1)(N+1)^m\implies\log\left|B_N\right|\ll m\log N\ll\sqrt{N}\log N. >$$

So, $\left|A_N\right|\ll\sqrt{N}\log N$. Now, for $N=2^k$,

$$> \left|A\cap\{0,\,\dots,\,2^k\}\right|=\sum_{n\leq k}\left|A_{2^n}\right|\ll\sum_{n\leq k}2^{n/2}n\ll k2^{k/2}. >$$

Thus,

$$> \frac{\left|A\cap\{0,\,\dots,\,2^k\}\right|}{2^k}\ll\frac{k}{2^{k/2}}\to 0, >$$

so $A$ has natural density zero. If $a\leq N$ and $a\in(B+B)$ with $B\subseteq\mathbb{N}_0$, then in fact, $a\in((B\cap[0,N])+(B\cap[0,N]))$ because $a=(b+b')\leq N$ with $b,b'\geq 0$ forces $b,b'\leq N$. Now assume $A\subseteq(B+B)$. If $\left|B\cap[0,N]\right|\leq\varepsilon\sqrt{N}$ for all large dyadic $N$, set $B_N:=B\cap[0,N]$, then $B_N\in\mathcal{B}_N$. But, $A_N\subseteq A$ and $A\subseteq B+B$ implies $A_N\subseteq B+B$. By the above, $A_N\subseteq B_N+B_N$, which is a contradiction. Therefore, for infinitely many (dyadic) $N$,

$$> \left|B\cap\{0,\,\dots,\,N\}\right|\geq\varepsilon\sqrt{N}\implies\limsup_{N\to\infty}\frac{\left|B\cap\{0\,\,\dots,\,N\}\right|}{\sqrt{N}}\geq\varepsilon, >$$

as claimed. $\square$

(The site has been updated to address this comment.)

The formal statement. The file's main theorem, not_erdos_333, asserts of one fixed set $A$, the union over $n\ge 3$ of finite sets chosen inside the dyadic intervals $(2^{n-1},2^n]$, that its counting function on $\{0,\ldots,N\}$ divided by $N$ tends to zero and that there is no $B\subseteq\mathbb{N}$ with $A\subseteq\{b+b' : b,b'\in B\}$ whose counting function on $\{0,\ldots,N\}$ divided by $\sqrt N$ tends to zero. The earlier file for Lean and Mathlib v4.29.1, linked second above, states the same theorem as main_obstruction; the later revision renames it, keeps main_obstruction as an alias, and changes only the lemma J_card_eq_half, whose proof is rewritten and whose unused positivity hypothesis is dropped. The formal-conjectures statement file for the problem names this development as the formal proof of its erdos_333 statement, tagged research solved, and the site's label carries a Lean qualifier. The statement allows $0$ as an element and counts $B\cap\{0,\ldots,N\}$; the thread had first asked which convention for $\mathbb{N}$ the problem intends, since with $B$ restricted to positive integers the set $A=\{1\}$ would be a trivial counterexample.

Acceptance. Formalized. This corpus's verification built the src/latest folder of Boris Alexeev's lean-proofs repository at the commit pinned first above (2026-09-15; Lean v4.33.0, Mathlib v4.33.0) and checked the axioms of Erdos333.not_erdos_333, which are exactly propext, Classical.choice and Quot.sound. The repository's comparator challenge for the problem pins that declaration, and the fingerprint of its type and of every definition the type reaches (the set $A$, its dyadic blocks, the counting function and the constants of the construction) was found identical in the challenge and in the solution; the theorem exists_hard_set, which the definition of the blocks invokes, is compared by type only, since its proof differs between the two files. The statement was audited clause by clause against the problem's Statement: it concerns one fixed witness $A$, which is exactly what a disproof needs, and with natural density zero, $0$ allowed in $B$ and $b=b'$ allowed it is the strongest form of the counterexample, so it answers the question no under every convention for $0$, for density and for $b=b'$; the challenge and solution statements agree apart from noncomputable markers and an inlined letI instance. What was built is the later revision; the v4.29.1 file, whose theorem has the same statement, was not built. Not reviewed: the site's curator credits the disproof to Theorem 2 of Erdős and Newman (1977), recorded at Erdős and Newman 1977, and the site's commentary does not mention this construction. Not refereed: there is no refereed write-up.

Depends on. No page of this wiki.