---

Terence Tao, A set that represents all large integers multiple times by consecutive elements, manuscript dated 2026-02-24, announced on the site's discussion thread for the problem on 2026-02-23 and revised there on 2026-02-24 after corrections from the thread. Theorem 1.1 states that there is a set $A$ of positive integers such that every sufficiently large $n$ has $\gg\log n$ representations as a sum of consecutive elements of $A$. In the problem's notation this is $f(n)\gg\log n$ for all large $n$, so $f(n)\to\infty$ and $f(n)\geq 2$ for all large $n$: both questions are answered yes. The growth is sharp up to the constant, since for every $A$ the sums of consecutive elements starting at $a$ are at least $a$ apart, which gives $\sum_{n\leq x}f(n)\leq x\log x+O(x)$ (Tao's inequality (1.1), observed earlier on the thread).

The argument is probabilistic. A set containing each positive integer independently with probability $1/2$ already has $\asymp\log n$ representations for all $n$ outside a sparse exceptional set of each dyadic block, but the exceptional probabilities are not summable. Tao modifies the random set so that each exceptional $n$ receives representations of its own, imposing primality and coprimality conditions on the parameters of the added summands so that the added representations do not collide, and concludes with the Borel–Cantelli lemma. This outline is a reading aid, not proof coverage.

The manuscript follows two incomplete attempts on the same thread, by Chojecki with GPT-5.2 Pro (2026-02-11) and by Sothanaphan with GPT-5.2 Thinking (write-up posted 2026-02-18, after an announcement on 2026-02-17), both built on a strategy Tao had proposed on 2026-02-07; Tao's introduction records that neither reached a complete proof, and the site's proof-claims tab listed no proof claim for the problem on 2026-10-07. Chojecki's write-up is recorded as rejected (claim page) and Sothanaphan's as withdrawn ([[problems/additive_bases/E0358/claims/2026_02_18_sothanaphan|claim page]]).

Dispute. On 2026-03-27 AronBhalla reported in the thread that running the 2026-02-24 manuscript through GPT 5.4 Thinking (named in the post as "5.4 Thinking") found the middle-range step in the proof of Proposition 3.1 false as written: the text asserts that for $q^{-1.4}\le|\theta|\le10/q$ the progression $(q-j)\theta$ stays $\gg q^{-0.4}$ from the integers for $q/40\le j\le q/20$, but $q=100$, $\theta=1/97$, $j=3$ gives $(q-j)\theta=1$, so the displayed bound $\ll\exp(-cq^{0.2})$ is not established by the argument as it stands; the report proposes a counting argument over $\gg q$ values of $j$ as the repair and lists smaller errors (a variable mismatch in Lemma 2.4(a), a wrong cross-reference after Proposition 2.1, the symbol $\Delta_{k'}$ for $R_{k'}$ in Proposition 2.2(i), the word "representing" dropped from the definition of $G_{n_p}$, and an unwritten counting step in Lemma 4.2). Tao replied the same day that these will be corrected in the next revision of the manuscript. No revised manuscript is linked from the site's page (last edited 2026-04-01) or from the formal-conjectures file, both of which cite the 2026-02-24 file, so the step stands disputed in the posted text. The Lean file linked below proves erdos_358 (a strictly increasing $A$ with $f(n)\to\infty$) and erdos_358_part_ii ($f(n)\ge2$ for all large $n$), which is what the problem asks, and not the bound $f(n)\gg\log n$; so the answer to the problem does not rest on the disputed step, while Theorem 1.1's logarithmic bound does.

Acceptance. The site's curator, T. F. Bloom, recorded the construction on the problem page (last edited 2026-04-01) under the label PROVED (LEAN), and the formal-conjectures statement file, pinned above at its last change (2026-09-18), tags both parts of the problem research solved, pointing for the formal proof to the pinned file in Boris Alexeev's lean-proofs repository (Lean 4.33.0, Mathlib v4.33.0). That file's header presents it as a formalization of a solution to the problem and credits Tao as the informal author, the formal-conjectures authors for the statement, and the AI systems Codex and GPT-5.6 Sol as the formal authors, so it is linked here as the formalization of Tao's result. The curator's record is the site's acceptance, named here as the reviewed evidence. This corpus has not built, replayed or audited the Lean file, so formalized is not listed, and no refereed publication exists.

Depends on. Nothing in this wiki.