Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
David Turturean's write-up proves (Theorem 1.1) that for every integer and every real there is a set of positive integers that is an additive basis of order in the site's sense, every large integer being a sum of at most elements of , has for all sufficiently large , where counts the nondecreasing representations of as a sum of at most elements of , and contains no minimal additive basis of order . This is the negation of the statement of Problem 870 for every : no constant exists. The input is the order-two basis of Larsen and Larsen, repaired for the at-most-two convention (Lemmas 2.1 and 2.2, Proposition 2.3). For a finite filler reduction (Lemma 5.1, Proposition 5.2) takes , so that a rigid residue class modulo forces every order- subbasis to project to an at-most-two subbasis of ; for , where the filler is unavailable, Proposition 4.1 replaces each canary element by a cluster of finitely many shifts and excludes the off-diagonal accidental representations by a summable Borel–Cantelli bound (Lemmas 3.1–3.3, Proposition 3.4). Section 6 assembles the theorem from Propositions 4.1 and 5.2. The source card is turturean_2026_negative_answer_erdos_problem_870.
Submission note. Posted to the site's forum by David Turturean on 24 April 2026:
LATER UPDATE (May 2): I have updated the write-up to address the concerns that explicitly or implicitly had to do with the k=3 case; as small as it is, it takes way longer to justify than k>=4, which all fall with a simpler argument. The Overleaf link stays the same, and the original version of the write-up can be found under main_apr24.pdf at the same link, while main.pdf is the newest version. The writing is still convoluted, and I verified this new version of the write-up by my own judgment and by scrutinizing it (wholly, or parts of it) using GPT-5.5-Pro. I aim to make it more human-parsable when time allows.
ORIGINAL COMMENT: I claim a solution to this problem, specifically a total refutation: the answer is no, for all . The writeup is at this Overleaf link.
The proof was developed via an automated multi-turn scaffold that I built, which iteratively queried ChatGPT-5.4-Pro (Extended Thinking), then, starting yesterday, ChatGPT-5.5-Pro (Extended Thinking) running in total for approximately 40+ consecutive turns/prompts (about 20 for each model).
The constructions in all cases ( and ) are inspired by the Larsen-Larsen 2026 robust order-2 basis without minimal subbases (their resolution of Erdős Problem #868), combined with (i) a finite filler gadget lifting to every , and (ii) a finite-shift clustered canary strengthening handling .
Here is GPT-5.5-Heavy Thinking verifying the solution: check 1, check 2, check 3. (I would have used Pro for verification but I used it so much that I got rate-limited, no joke...)
I have been attempting a Lean 4 / Mathlib Aristotle-based autoformalization, but it is hindered by the fact that the underlying Larsen-Larsen (2026) preprint is itself not straightforwardly formalizable, likely related to how it is a probabilistic random-construction argument; comments on the #868 page note the same formalization obstacle.
Status of the claim. The write-up was posted to the problem's thread on
2026-04-24. Turturean reports that it came from an automated multi-turn
scaffold Turturean built, which queried ChatGPT-5.4-Pro (Extended Thinking) and
then ChatGPT-5.5-Pro (Extended Thinking). Daniel Larsen replied on 2026-04-25
that one claim in the write-up looked doubtful to Larsen, and Turturean revised
the case at the same link on 2026-05-02. The claimant's repository (pinned
above, 2026-06-26) holds the paper and a Lean 4 development whose final
declaration Erdos870.erdos_870 states the negation in the at-most-
convention. The repository states that Turturean is responsible for the final
mathematical claims and exposition, describes the development as free of
admitted proofs with kernel dependencies propext, Classical.choice and
Quot.sound, and names GPT-5.4-Pro and then GPT-5.5-Pro for the
natural-language proof and GPT-5.5-Pro, Codex (GPT-5.5-xhigh) and Claude Code
(Opus 4.8, maximum thinking) for the Lean. Johan Land reported on the thread
on 2026-09-01 that Land had validated the formalization as a full solution of
the at-most- reading. This corpus has not built or audited the Lean, the
site labels the problem OPEN, and there is no refereed publication.
The claim answers the site's at-most- wording only. It does not address the version in [ErNa88], with sums of elements and disjoint representations (see the problem page's Formulation).
Depends on. Larsen and Larsen, whose order-two construction is the input.