---

Claim. The answer to Problem 871 is no: there is an additive basis $A$ of order $2$ with $1_A\ast 1_A(n)\to\infty$ that cannot be partitioned into two disjoint additive bases of order $2$. In the Lean statement not_erdos_871, $A$ is a set of natural numbers such that every sufficiently large $n$ is a sum $a+b$ with $a,b\in A$, such that for every $t$ every sufficiently large $n$ has at least $t$ pairs $a\le b$ in $A$ with $a+b=n$, and such that no disjoint $B,C$ with $A=B\cup C$ both represent every sufficiently large integer as a sum of two of their elements. Counting pairs with $a\le b$ differs from $1_A\ast 1_A(n)$ by at most a factor of two, so the divergence is the one the problem asks for.

Submission note. Posted to the site's forum by Daniel Larsen on 5 January 2026:

This seems to be an LLM-generated formal proof. (Statement on line 4930.)

It follows the Erdős-Nathanson method extremely closely, but lets the size of $F_k$ go to infinity very slowly. The same method should resolve the first half of [868] (courtesy of Claude Opus 4.5). In particular, the $F_k$ instead of being an enumeration of $t$-element subsets of $[1,g(t)]\cap A$ over all $t$ should be an enumeration of $t$-element subsets of $(g(t-1),g(t)]\cap A$. For $B\subset A$, being a basis is equivalent to $A\setminus B$ having fewer than $t$ elements in $(g(t-1),g(t)]$ for all but finitely many $t$. This property is stable under removal of finite subsets.

Argument. Erdős and Nathanson had proved (erdos_1989_additive_bases_many_representations) that for every fixed $t$ there is a basis of order $2$ with $1_A\ast 1_A(n)\ge t$ for all large $n$ that cannot be split into two disjoint bases, and had asked (erdos_1988_partitions_bases_into_disjoint_unions_bases) whether divergence suffices, having proved that it does once the number of representations $n=a+a'$ with $a\le a'$ in $A$ is at least $c\log n$ for all large $n$, for some constant $c>1/\log(4/3)$. The disproof keeps their construction and lets $t$ grow slowly. A base set $B$, a union of long and widely spaced intervals with a few elements removed, has a representation function that vanishes on a rapidly growing sequence $N_1<N_2<\cdots$ and tends to infinity elsewhere. To $B$ one adds a few elements so that each $N_k$ gains exactly $t(k)$ representations, through a $t(k)$-element set $A_k$ with $N_k-A_k\subseteq A$, where $t(k)\to\infty$ slowly and the sets $A_k$ run through all $t$-element subsets of successive blocks of the set. Whenever $A$ is split into two parts, the pigeonhole principle puts some $t(k)$-subset of each block wholly inside one part, and the other part then contains no element of that $A_k$; so for infinitely many $k$ one fixed part contains no element of $A_k$ and cannot represent $N_k$, and that part is not a basis. The curator's remark that only a small modification of the 1989 argument is needed, and a sketch of this shape posted on the thread by Tao on 2026-01-05, are the sources of this outline; it is a reading aid, not proof coverage.

The postings. The claimant posted the Lean proof to the problem's thread on 2026-01-05 as a Lean playground link, with the statement on line 4930 of the file (the first formalization link is that post; the playground address encodes the whole file and is too long to reproduce), and the system's write-up the same day (the first preprint link, a GitHub upload of 2026-01-05 that Larsen described as stylistically flawed); the system's original solution, a LaTeX write-up produced from the problem statement and the 1989 paper, was uploaded on 2026-01-06 (the second preprint link). On the thread Larsen described the system as Claude and Gemini agents with assigned roles and Larsen's own part as reading the Erdős–Nathanson paper, directing the system to formalize the relevant parts and to extend the construction, and intervening when the formalization went off track. Larsen's later preprint (larsen_2026_three_questions_erdos_nathanson_asymptotic_bases, arXiv:2603.03472, 2026-03-03, 7 pages) records the result as the author's, obtained with the multi-agent system, and proves more by a different construction: a divergent representation function, decomposability into two disjoint bases, and containing a minimal basis are mutually independent properties of asymptotic bases of order $2$, every combination being realized (its Theorem 1). That preprint is a second, unrefereed proof of the same answer and is linked here rather than given its own page.

Acceptance. The reviewed evidence is the site's acceptance: its curator, Thomas Bloom, credits the disproof to Larsen using Claude Opus 4.5 in the problem's remarks, and the page carries the label DISPROVED (LEAN) (last edited 2026-01-06). The formal-conjectures statement file (the record link, pinned at its revision of 2026-10-06) tags erdos_871 research solved with the answer False and records a formal proof at the Lean file below; the statement itself is left as sorry there, so the record is a catalog entry and not a formalization. On the thread, Tao noted on 2026-01-05 that the result is a disproof rather than a proof and sketched the argument; Tao did not report checking the Lean file, which exceeded the heartbeat limit when Tao ran it. Alexeev reported that every native_decide call in the first Lean file could be replaced by decide or norm_num. No named mathematician has reviewed the write-ups and there is no refereed publication.

Formalization. The second formalization link is the file src/v4.29.1/ErdosProblems/Erdos871.lean of Boris Alexeev's repository https://github.com/plby/lean-proofs, a later revision of the playground file, shorter and without native_decide, added to the repository on 2026-05-12 (the link's date) and pinned at the commit of 2026-06-24 that gave the folder its name (Lean 4.29.1). Its header declares it a Lean formalization of a solution to the problem and names Erdős, Nathanson, Larsen and Claude Opus 4.5 as informal authors and Claude Opus 4.5, Gemini 3 Pro and Larsen as formal authors, so it is a formalization of the claimant's result and is linked here rather than given its own page. At the pinned revision the file imports only Mathlib, its 2,415 lines contain no sorry and no native_decide, and its closing #print axioms comment records propext, Classical.choice and Quot.sound for not_erdos_871, whose conclusion is the negation of the universal clause of the catalog's erdos_871. This corpus has not built the file, printed its axioms or audited its definitions, so the claim carries no formalized evidence and the formalization is a link, not a warrant.

Depends on. Nothing in this wiki; the construction is self-contained apart from the 1989 paper it modifies.