---

Claim. The answer claimed is no. For the seed

$$A=\{1,2,3,5,7,13,22,27,28,32,36,40,47,48,52,63,71,77,81,89,97\},$$

the sequence of Problem 341, $a_{n+1}=\min\{t>a_n:t\notin A_n+A_n\}$ with $A_n=\{a_1,\ldots,a_n\}$ and equal summands allowed (the problem's $i,j\le n$ permits $i=j$), has gaps $d_m=a_{m+1}-a_m$ such that for every $K\ge1$ and $h\ge1$ some $m\ge K$ has $d_{m+h}\ne d_m$; so the gap sequence is not eventually periodic. This is Theorem 1.1 of Zhiheng Li, Counterexamples to Erdős Problem 341, a seven-page paper in the claimant's repository at the commit of 20 August 2026 linked above (first uploaded 9 August 2026). The method: Lemma 1.2 shows that an infinite $S\subseteq\mathbb N$ with $97\in S$ and $t\in S$ exactly when $t\notin S+S$ for every $t>97$ is the greedy extension of $S\cap[1,97]$; the paper builds such an $S$ from a scale-eight controller, the sets $Y_0=\{0\}\cup\bigcup_k[4\cdot8^k,8\cdot8^k-1]$, $Y_1=(Y_0+Y_0)^c$ and $Y_2=(Y_1+Y_1)^c$, which satisfy $Y_0=\{0\}\cup(1+(Y_2+Y_2)^c)$ (Lemma 2.1), embedded in three residue classes modulo $49$ and protected by a finite modular shield (Section 3). The indicator of $Y_0$ is not ultimately periodic (Lemma 2.2: for $a=8^k$ larger than the putative threshold and period $h$, the integer $4a-h$ lies outside $Y_0$ while $4a$ lies inside), and the aperiodicity transfers to $S$ and to its gaps. A modification gives an infinite family of seeds $A_p$ with a shield modulo $7p$ for every $p\ge18$ (the paper's Theorem 5.1, as the repository's README states it).

Submission note. Posted to erdosproblems.com as a proof claim by Zhiheng Li (account Z_Li) on 9 August 2026, giving "GPT-5.6 Sol" as the AI used:

We construct an explicit finite set of positive integers whose greedy pair-sum-avoiding extension has a non-eventually periodic sequence of consecutive gaps. The construction consists of a nonperiodic scale-eight sumset controller embedded in three residue classes modulo $49$, together with a finite modular shield. For the fixed $21$-element seed

$$> \begin{split} A=\{&1,2,3,5,7,13,22,27,28,32,36,40,47,48,52,\\ > &63,71,77,81,89,97\}, \end{split}$$

we give an explicit infinite set $S$,

prove $t\in S\Longleftrightarrow t\notin S+S$ for every $t>97$, and prove that the membership indicator of $S$ is not ultimately periodic. The exact recurrence verifies the least-admissible-next-term rule, with equal summands allowed, and implies that the gap sequence of the greedy extension is not eventually periodic.

The formalization. LeanProject/Erdos341.lean (847 lines), with Erdos341Shield.lean (the finite residue certificate) and Erdos341g.lean (the family), in the same repository. The final theorem Erdos341.erdos_341_negative states that the set $S$ is the greedy extension of the seed with threshold $97$, that the enumeration of $S$ follows the least-admissible-next-term rule from the index of $97$ on, and that the gap function, the difference of consecutive values of the enumeration, is not eventually periodic; Erdos3417p.theorem_5_1_nonperiodicity is the family's theorem. The README reports the axiom list propext, Classical.choice, Quot.sound for both, no sorry, admit, custom axiom or native_decide, finite certificates by kernel decide, and toolchain v4.33.0-rc1; the development is archived on Zenodo (version 2.0.1, 20 August 2026, CC BY 4.0). The three files contain no sorry, axiom or native_decide. This repository is not built by this corpus, and the fidelity of its definitions of the greedy extension and of eventual periodicity to the problem's rule is not audited; the acceptance below rests on the build of the second development, which carries the fixed-seed files. The proof-claim tab lists GPT-5.6 Sol as the AI system used, and the paper's AI disclosure says that the proof was developed with the system's assistance and checked by the author.

A second development, the file src/latest/ErdosProblems/Erdos341.lean of Boris Alexeev's public repository plby/lean-proofs, linked at the pinned commit (added 2026-08-26; Lean v4.33.0, Mathlib v4.33.0), declares itself a formalization of this result: its header names Li, with GPT-5.6 Sol, as the author of the negative answer, Li's repository at the revision linked above as its source and the proof-claim post as the claim. Its component modules Erdos341/Proof.lean (847 lines, ending in Li's theorem erdos_341_negative) and Erdos341/Shield.lean (the finite shield certificate) carry Li's fixed-seed development; the family file is not included. Its theorem not_erdos_341, assembled from Li's lemmas, exhibits a strictly increasing sequence of positive integers that follows the least-admissible-next-term rule from some index on, with equal summands allowed, and whose gap sequence is not eventually periodic.

Acceptance. Formalized. This corpus's verification built Alexeev's repository at the pinned commit 8822f7dd (2026-09-15; folder src/latest, Lean v4.33.0, Mathlib v4.33.0): the solution module ErdosProblems.Erdos341 with its two component modules, and the comparator challenge ComparatorChallenges/ErdosProblems/Erdos341.lean. The axioms of Erdos341.not_erdos_341 are exactly propext, Classical.choice and Quot.sound, and its fingerprint is identical to the challenge's, whose statement uses Mathlib's vocabulary alone, with no custom definitions. The statement was audited clause by clause against the problem's Statement. It gives a strictly increasing sequence $a:\mathbb N\to\mathbb N$ of positive integers and an index $k$ such that for every $n\ge k$ the term $a(n+1)$ is the least integer above $a(n)$ that is not $a(i)+a(j)$ with $i,j\le n$ (equal summands allowed, as in the Statement), and the gaps $a(n+1)-a(n)$ are not eventually periodic; the natural-number subtraction is exact because $a$ increases. The rule fixes every term after the $k$-th, so $a$ is the greedy extension of the seed $\{a(0),\ldots,a(k)\}$, and one such seed answers the question no, which is the full claim. The theorem does not name Li's seed, though its proof uses it. What was built is Alexeev's development, not Li's repository: Li's own files at toolchain v4.33.0-rc1 and the family theorem were not built. The challenge's configuration switches off an independent second-kernel re-check, which this acceptance does not use. Not reviewed: the site's label was OPEN on 2026-10-07 (page last edited 20 January 2026), with no comment under the claim on the proof-claims tab, and the formal-conjectures collection's research solved tag of 2026-09-18, which credits Li and points its formal_proof attribute at Alexeev's file, is a catalog entry, not a review; the tagged statement at that commit, which records the answer as false, is not audited here. Not refereed: the paper is posted in the claimant's repository and archived on Zenodo, and no journal publication was found.

Scope. Full: the problem asks whether the differences are eventually periodic for every finite seed, and one seed with aperiodic gaps answers no.

Depends on. No page of this wiki.