---

Claim. There is an infinite admissible set $A=\{a_1<a_2<\cdots\}\subset\mathbb N$, in the sense of Problem 875 (the sums of $r$ distinct members are disjoint for distinct $r$), with

$$a_{n+1}-a_n\le n^{3+2\sqrt2}\quad(n\ge1) \qquad\text{and}\qquad a_{n+1}-a_n=o\bigl(n^{3+2\sqrt2}\bigr),$$

the note's Theorem 1, with $3+2\sqrt2=5.828\ldots$. So the exponent $c=3+2\sqrt2$ is possible in the problem's last question, in the reading "for all $n$" as well as "for all large $n$", below the eventual exponents $c>5+2\sqrt6=9.899\ldots$ that the problem page extracts from the density of the Erdős--Nicolas--Sárközy construction on the card erdos_1991_sommes_de_sous_ensembles. The note's corollary adds that the constructed set has $a_n=o(n^{4+2\sqrt2})$, that is $A(x)=|A\cap[1,x]|=\omega(x^{1/(4+2\sqrt2)})$, obtained by summing the little-o gap bound, and compares the exponent $1/(4+2\sqrt2)=0.1464\ldots$ with the growth exponent $5-2\sqrt6=0.1010\ldots$ of the Erdős--Nicolas--Sárközy construction, which it would improve. The construction is by blocks: each block has large internal multiplicative spread, the gap between consecutive blocks equals the internal spacing of the block before it, and admissibility is proved by a carry invariant for differences of subset sums graded by cardinality; a finite prefix makes the pointwise bound hold from $n=1$. The note itself says that the exponent is not claimed to be optimal and that the sequence's consecutive ratios have unbounded $\limsup$, so it says nothing about the ratio condition $a_{n+1}/a_n\to1$. The note lists GPT-5.5 Pro, a large language model by OpenAI, as its first author, stating that it performed nearly all of the derivation and drafting through prompted interaction, and Lech Mazur as prompter and curator; the claimant here is the human who posted it. The repository, at the revision linked above (its head of 2026-05-09), carries the note under docs/, a Lean 4 development whose Solution.lean proves the declaration AdmissibleCarry.published_final_construction stated in Challenge.lean over Mathlib, a statement map, an assumptions audit and a comparator configuration; its statement map says the formal theorem gives an infinite admissible set with a strictly increasing enumeration, the normalized gap limit and the all-index pointwise bound with denominator $(n+1)^{3+2\sqrt2}$ for a zero-indexed enumeration, and that the all-index bound is proved for a prefixed sequence rather than the unprefixed one. The README says that generative AI tools assisted the development, and the thread post of 2026-05-07 names Codex for the formalization. Read status: the README, the statement map and the note's statements checked; the proofs unread.

Covers. The gap question and, through the corollary, the growth question: some admissible sequence has $a_{n+1}-a_n\le n^{3+2\sqrt2}$ for every $n$, so every exponent $c\ge3+2\sqrt2$ is possible, and the same sequence has $A(x)=\omega(x^{1/(4+2\sqrt2)})$, which would improve the growth exponent $5-2\sqrt6$ of the Erdős--Nicolas--Sárközy construction. The claim does not determine the set of possible exponents, which on the problem page stays open between the necessary $c\ge1$ and this bound, nor how dense an admissible set can be at most, and it does not address whether $a_{n+1}/a_n\to1$ is attainable.

Depends on. No page of this wiki: the block construction is self-contained, and the Erdős--Nicolas--Sárközy construction it improves on is cited for comparison only.

Standing. Claimed. The note and repository were announced in the site's discussion thread on 2026-05-07 and are not on the proof-claims tab, which is empty; the site's label is OPEN and its commentary does not mention them (as of 2026-10-06). A thread commenter reported on 2026-05-08 that a ChatGPT check found no issue in the note but that the Lean file then stated only the little-o part of Theorem 1, and the poster reported the formalization extended to the pointwise bound on 2026-05-09; neither exchange is a review. The Lean development is third-party Lean that this corpus has not built or audited, so it gives no formalized evidence. No preprint-server or journal record of the note was found on 2026-10-07.