Erdoes #875 - working report - Erdős Problem a Day

Erdős problem #875 — wave 7q

Date of live-page check: 2026-07-27 UTC.

Result in one paragraph

[a: elementary-rigorous] I prove a sharp barrier for the entire C_k carry-block framework used by the currently best posted construction, not merely for its particular power-law schedule. If

C_k=\{1+i(k+1):0\le i<k\},\qquad Q_k=k^2+k+1,

and every stage is certified by the posted carry-closure hypothesis, then every choice of block sizes satisfies

\limsup_{j\to\infty} \frac{\log\bigl(M_j(k_j+1)\bigr)} {\log(N_{j-1}+1)} \ \ge\ 3+2\sqrt2.

Here $M_j(k_j+1)$ is the first internal gap of block $j$, at sequence index $N_{j-1}+1$. Consequently no rescheduling of these same blocks under this same closure lemma can prove a bound $a_{n+1}-a_n\le n^c$ with $c<3+2\sqrt2$. [b: modulo the checked theorem AdmissibleCarry.published_final_construction] The posted construction attains $c=3+2\sqrt2$ and even has little-$o$ gaps, so this exponent is exact for this framework. This does not settle the original problem: the global known interval remains

1\le c_{\mathrm{possible}}\le 3+2\sqrt2

in the sense detailed below, and the range $1\le c<3+2\sqrt2$ remains open.

Claim labels used throughout:

[a] elementary-rigorous;
[b] rigorous modulo the named published theorem;
[c] plausible/structural-unverified;
[d] computational-only or direct webpage/search observation.

Step 0: authoritative live page

The page was fetched through the Bright Data browser path, not datacenter curl. The rendered main page, the separate discussion thread, the link targets, a screenshot, and the site's LaTeX-source view were all inspected.

Verbatim statement

The following is copied verbatim from the site's LaTeX-source view:

Let $A=\{a_1<a_2<\cdots\}\subset \mathbb{N}$ be an infinite set such that the sets\[S_r = \{ a_1+\cdots +a_r : a_1<\cdots<a_r\in A\}\]are disjoint for distinct $r\geq 1$. How fast can such a sequence grow? How small can $a_{n+1}-a_n$ be? In particular, for which $c$ is it possible that $a_{n+1}-a_n\leq n^{c}$?

The accompanying text, also copied verbatim, is:

A problem of Deshouillers and Erd\H{o}s (an infinite version of [874]). Such sets are sometimes called admissible. Erd\H{o}s writes 'it [is not] completely trivial to find such a sequence for which $a_{n+1}/a_n\to 1$'. It is not clear from this whether Deshouillers and Erd\H{o}s knew of such a sequence.

Stop-condition audit

[d: direct live-page observation]

Live field	Value on 2026-07-27
Status	`OPEN`
Comments	7
Claimed proofs	0
Interested in collaborating	None
Currently working on this problem	None
Working on formalising	None

Thus neither mandatory stop condition applied.

All seven comments

[d: direct discussion-page observation]

Lech Mazur, 7 May 2026: a GPT-5.5 Pro/harness note claims an explicit

infinite admissible set with $a_{n+1}-a_n=o(n^{3+2\sqrt2})$, emphasizing that this is about absolute gaps and not $a_{n+1}/a_n\to1$.

MalekZ, 8 May: asks which harness was used.
Lech Mazur, 9 May: describes the harness.
MalekZ, 11 May: brief harness follow-up.
Nat Sothanaphan, 8 May: reports no issue from a standard check, but notes

that the first Lean version formalized the little-$o$ assertion and not the stated all-index pointwise bound.

Lech Mazur, 9 May: reports that the Lean statement and proof were updated

to include the all-index pointwise bound.

Aron Bhalla, 24 February 2026: points to the 1991

Erdős–Nicolas–Sárközy infinite construction and the 1999 Deshouillers–Freiman sharp finite theorem.

The first six displayed entries include three nested harness replies; together with the February literature comment they are the site's seven comments.

Authoritative URLs:

live problem: <https://www.erdosproblems.com/875>
discussion: <https://www.erdosproblems.com/forum/thread/875>
posted proof artifact: <https://github.com/lechmazur/erdos_875>

Literature and artifact audit

Original source

[d: bibliographic verification] The site's [Er98] is:

P. Erdős, Some of my new and almost new problems and results in combinatorial number theory, in Number Theory: Diophantine, Computational and Algebraic Aspects, de Gruyter (1998), pp. 169–180, DOI <https://doi.org/10.1515/9783110809794.169>.

The publisher metadata was checked. The live page, rather than a guessed reconstruction from this paywalled chapter, is used as the statement of record.

Erdős–Nicolas–Sárközy (1991)

[b: Theorem 2 of the named paper] P. Erdős, J.-L. Nicolas, and A. Sárközy, Sommes de sous-ensembles, J. Théorie des Nombres de Bordeaux 3 (1991), 55–72, DOI <https://doi.org/10.5802/jtnb.42>, really states that there is an infinite admissible $A$ with

A(x)\gg x^{5-2\sqrt6}.

I inspected the theorem on printed page 65 of the primary Numdam PDF. The exact inspected file has SHA-256 176829aac870e1a120fa4f547d32b575f09a664a3f0a74d3dec32c0eaa9bc81c.

[a, from that theorem] Since

\frac1{5-2\sqrt6}=5+2\sqrt6,

this gives $a_n\ll n^{5+2\sqrt6}$, hence the crude absolute-gap bound $a_{n+1}-a_n=O(n^{5+2\sqrt6})$. The implicit constant means that the literal coefficient-one inequality follows immediately for every exponent $c>5+2\sqrt6$, not necessarily at the endpoint from this deduction alone. Polynomial growth also implies $\liminf a_{n+1}/a_n=1$: ratios bounded below by $1+\epsilon$ eventually would force exponential growth.

Deshouillers–Freiman (1999)

[b: Theorem 1 of the named paper] J.-M. Deshouillers and G. A. Freiman, On an additive problem of Erdős and Straus, 2, Astérisque 258 (1999), 141–148, DOI <https://doi.org/10.24033/ast.442>, proves that for all sufficiently large $N$, every admissible $A\subset[1,N]$ satisfies

|A|\le 2\sqrt{N+\tfrac14}-1.

This was read directly from printed page 142 of the primary Numdam PDF. The inspected file has SHA-256 b376104edc3ba632f15b490d75de53b38dfd0b801dc143c24702d638435b29da.

[a, from that theorem] Applying the finite bound to $\{a_1,\ldots,a_n\}\subset[1,a_n]$ yields

a_n\ge (1/4-o(1))n^2.

If $a_{n+1}-a_n\le n^c$ eventually with $c<1$, summation would instead give $a_n=O(n^{c+1})=o(n^2)$, a contradiction. Thus $c\ge1$ is necessary.

May 2026 carry construction

[d: fresh machine audit] I cloned the repository at commit d450886bd73e7a188b8b8bbe7b9aec771d3b06a1 and ran its pinned Lean 4.30.0-rc2/mathlib build:

lake exe cache get
lake build AdmissibleCarry Challenge Solution
bash scripts/audit_sorries.sh .
bash tools/check_no_sorry.sh
bash scripts/audit_imports.sh .

All 8,335 build jobs completed successfully. Both placeholder scans reported no sorry, admit, axiom, or unsafe occurrence in the proof library. Challenge.lean itself intentionally contains the trusted statement as a sorry, and the build reports that warning; Solution.lean proves the identical public statement from the checked library. I did not rerun the repository's optional external comparator.

[b: named checked theorem] AdmissibleCarry.published_final_construction states an infinite admissible set, a strictly increasing enumeration, the normalized gap limit $0$, and the all-index pointwise bound at exponent $3+2\sqrt2$. Thus the current verified upper endpoint is

c=3+2\sqrt2=5.828427124746\ldots.

Search miss

[d: search observation, not an exhaustiveness theorem] Exact-title, exact-problem-number, and phrase searches for infinite subset-cardinality admissible sets found the two primary papers above and the May 2026 artifact. Other prominent results used “admissible” in the unrelated prime-tuples sense. I found no additional primary source improving the absolute-gap endpoint. This is an honest search miss, not a claim that no such source exists.

New result: schedule-optimality of the posted carry blocks

Framework

Fix a finite prefix $A_0\subset[1,M_1)$. For arbitrary positive integers $k_j$, define

\begin{aligned} C_k&=\{1+i(k+1):0\le i<k\},\\ Q_k&=k^2+k+1,\\ B_j&=M_jC_{k_j},\\ A_j&=A_{j-1}\cup B_j,\\ M_{j+1}&=M_jQ_{k_j},\\ N_j&=|A_j|=N_0+\sum_{i\le j}k_i. \end{aligned}

Assume every stage is certified by the carry-closure lemma's hypothesis

\frac{\Sigma(A_{j-1})}{M_j}<\frac{k_j}{4}. \tag{H}

No power law or regularity assumption is made on the sequence $k_j$.

Theorem

[a: elementary-rigorous] Every schedule satisfying (H) obeys

\boxed{\quad \limsup_{j\to\infty} \frac{\log\!\left(M_j(k_j+1)\right)} {\log(N_{j-1}+1)} \ge 3+2\sqrt2. \quad} \tag{1}

The numerator is the logarithm of an actual consecutive gap whose left endpoint has index $N_{j-1}+1$. Hence an eventual pointwise bound $a_{n+1}-a_n\le n^c$ in this framework forces

c\ge3+2\sqrt2. \tag{2}

Proof, part 1: closure forces doubling

Put

s_j=\frac{\Sigma(A_{j-1})}{M_j}.

The block identities

\Sigma(C_k)=\frac{k^3+k}{2},\qquad Q_k=k^2+k+1

give the exact recurrence

s_{j+1} =\frac{s_j+(k_j^3+k_j)/2}{Q_{k_j}}. \tag{3}

For every $k\ge1$,

\frac{k^3+k}{2(k^2+k+1)}>\frac{k-1}{2}, \tag{4}

because

\[ (k^3+k)-(k-1)(k^2+k+1)=k+1>0. \]

Equations (3)–(4), positivity of $s_j$, and the next instance of (H) imply

\frac{k_{j+1}}4>s_{j+1}>\frac{k_j-1}{2}.

Since $k_{j+1}$ is an integer,

k_{j+1}-1\ge2(k_j-1). \tag{5}

Thus, with $h_j=k_j-1$, the $h_j$ at least double. In particular,

N_{j-1}+1=\Theta(h_{j-1}) \tag{6}

after discarding a finite prefix: the reverse geometric series gives $\sum_{i<j}h_i<2h_{j-1}+O(1)$, and the number of added $+1$'s is only $O(\log h_{j-1})$.

Proof, part 2: convert the actual gaps to a control recurrence

Blocks are globally ordered because

\max B_j=M_jk_j^2<M_jQ_{k_j}=M_{j+1}=\min B_{j+1}.

The first two elements of $B_j$ are $M_j$ and $M_j(k_j+2)$, so the first internal gap is

G_j=M_j(k_j+1) \tag{7}

at left-endpoint index

\nu_j=N_{j-1}+1. \tag{8}

By (5), $k_j\ge2$ eventually, so this gap always exists in the tail.

Choose a tail on which $h_j>1$, and write

x_j=\log h_j,\qquad S_j=\sum_{i=J}^{j-1}x_i.

Since $Q_{k_i}\ge h_i^2$, (6)–(8) give

\log G_j\ge2S_j+x_j+O(1),\qquad \log\nu_j=x_{j-1}+O(1). \tag{9}

Define

t_j=\frac{S_j}{x_{j-1}},\qquad r_j=\frac{x_j}{x_{j-1}}.

Then

t_{j+1}=1+\frac{t_j}{r_j}, \tag{10}

and the normalized lower-bound cost in (9) is

E_j=2t_j+r_j. \tag{11}

Proof, part 3: the discriminant obstruction

Suppose for contradiction that the limsup in (1) is below $3+2\sqrt2$. The $O(1)$ terms in (9) are negligible because $x_j\to\infty$. We may therefore choose a constant

3<C<3+2\sqrt2

such that $E_j\le C$ eventually. (If needed, $E_j>3$ follows from $t_j\ge1$ and $r_j>1$.)

From $2t_j+r_j\le C$,

r_j\le C-2t_j.

Substitution into (10) yields

t_{j+1}\ge F_C(t_j):= 1+\frac{t_j}{C-2t_j}. \tag{12}

Moreover,

F_C(t)-t =\frac{2t^2-(C+1)t+C}{C-2t}. \tag{13}

The numerator in (13) has discriminant

\Delta_C=(C+1)^2-8C=C^2-6C+1. \tag{14}

Its roots as a polynomial in $C$ are $3\pm2\sqrt2$. Therefore $\Delta_C<0$ for $3<C<3+2\sqrt2$, and the quadratic numerator in (13) has the positive minimum

m_C=-\frac{\Delta_C}{8}>0. \tag{15}

The cost bound also gives $0<C-2t_j\le C$, so (12)–(15) imply

t_{j+1}-t_j\ge\frac{m_C}{C}>0 \tag{16}

at every sufficiently large stage. This forces $t_j\to\infty$, while $2t_j+r_j\le C$ forces $t_j<C/2$, a contradiction. This proves (1).

Finally, a pointwise gap bound with exponent $c$ applies to the actual gaps $(G_j,\nu_j)$, so (1) implies (2). This completes the proof.

Sharpness inside the framework

[a: elementary-rigorous algebra] Equality is the stationary control:

r=1+\sqrt2,\qquad t=\frac r{r-1},\qquad t=1+\frac tr,\qquad 2t+r=3+2\sqrt2.

[b: checked posted theorem] The schedule

k_j=\left\lceil2(1+N_{j-1})^{1+\sqrt2}\right\rceil

in the May 2026 artifact attains the endpoint, with both

a_{n+1}-a_n\le n^{3+2\sqrt2} \quad\text{for every }n\ge1

and

a_{n+1}-a_n=o(n^{3+2\sqrt2}).

Together with (1), this classifies the coefficient-one exponents obtainable by this exact carry-block/closure framework:

\boxed{c\ge3+2\sqrt2.}

Independent checker and exact finite audit

The standalone checker is runs/erdos875_wave7q_reverify.py (SHA-256 413025a74d6810cc28c91b3df936c57c04d24d9c6c4b7efebf915278de87ba33). It uses only the Python standard library.

Run:

python runs/erdos875_wave7q_reverify.py
python runs/erdos875_wave7q_reverify.py \
  --max-local-k 8 --schedule-stages 4 --check-sources

The first command took 6.21 seconds and 22,408 KB maximum RSS on this VM.

What is recomputed

[d: computational-only]

All quadratic-surd identities, including

$(5-2\sqrt6)^{-1}=5+2\sqrt6$ and the barrier root.

Every reduced signed subset relation

$\epsilon\in\{-1,0,1\}^k$ for $1\le k\le12$: 797,160 relations in total. It directly checks admissibility of $C_k$ and every triggered case of the local-carry implication; 59,900 cases trigger its strict $(u,w)$ window.

Two complete closure stages from $A_0=\{1,2\},M_1=4$, with the smallest

legal block sizes $k_1=4,k_2=7$. The final set has 13 elements, $M_3=4788$, and sum 14,839. All $3^{13}=1,594,323$ signed relations are checked for carry-goodness; 537 are divisible by $M_3$, and all have the required defect.

The exact minimal strict-closure schedule:

$j$	$N_{j-1}$	$k_j$	$M_j$	$s_j$	first gap
1	2	4	4	$3/4$	20
2	6	7	84	$139/84$	672
3	13	13	4,788	$781/252$	67,032
4	26	25	876,204	$279241/46116$	22,781,304
5	51	49	570,408,804	$361136941/30021516$	28,520,440,200
6	100	97	1,398,071,978,604	$1767097332025/73582735716$	137,011,053,903,192

Exact rational subcritical discriminant certificates. For example,

$C=5$ has $\Delta_C=-4$, quadratic minimum $1/2$, and forces $t_{j+1}-t_j\ge1/10$; $C=29/5=5.8$ has $\Delta_C=-4/25$ and forces an increment at least $1/290$.

With --check-sources, fresh downloads of the two primary PDFs and their

exact SHA-256 digests.

The finite enumeration is an independent bug detector; the uniform theorem is the elementary proof above, not an extrapolation from these tests.

Exact remaining wall

[a: consequence of the new theorem] Merely changing the growth rate of the $k_j$ in the posted construction cannot improve its exponent. The power-law optimization in the posted note was already suggestive; the theorem above removes the power-law assumption and proves the full schedule barrier.

[c: structural diagnosis] An improvement below $3+2\sqrt2$ must change at least one substantive part of the mechanism:

replace $C_k,Q_k$ by a genuinely different local gadget;
strengthen the closure invariant so the post-block normalized sum does not

force $k_{j+1}-1\ge2(k_j-1)$; or

avoid placing an $M_j(k_j+1)$-sized gap immediately at index

$N_{j-1}+1$, for example through a non-block or interleaved transition.

The exact missing lemma is therefore a carry-compatible local transition that adds $k$ elements while simultaneously controlling:

cardinality-graded subset-sum differences;
the first element and all early consecutive gaps;
the next modulus/scale; and
the normalized old-error window,

with asymptotic parameters outside the recurrence proved above. Finite cardinality optimality alone is insufficient.

[d: computation-cost diagnosis] Blind gadget enumeration is already infeasible. At the present natural scale $Q_{12}=157$, testing every 12-element subset would mean

\binom{157}{12}=304{,}271{,}380{,}653{,}382{,}415

candidates. Even an unrealistic $10^8$ candidates/second would require about $8.45\times10^5$ core-hours, before checking any signed relations. A future computation needs SAT/CP symmetry reduction and a mathematically specified alternative invariant; this brute-force job was not run.

Honest scope

[a] This report proves an exact theorem for the strongest currently posted construction framework and isolates what a better construction must change. [b] Published finite theory rules out $c<1$, and the checked May 2026 artifact realizes $c=3+2\sqrt2$. [c] Nothing here establishes existence or nonexistence for $1\le c<3+2\sqrt2$, nor does the construction address $a_{n+1}/a_n\to1$. Therefore the original problem remains open.

PARTIAL: Proved that $3+2\sqrt2$ is the sharp exponent for every block-size schedule certified by the posted $C_k$ carry-closure lemma; the original range $1\le c<3+2\sqrt2$ remains open.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger

\(j\)	\(N_{j-1}\)	\(k_j\)	\(M_j\)	\(s_j\)	first gap
1	2	4	4	\(3/4\)	20
2	6	7	84	\(139/84\)	672
3	13	13	4,788	\(781/252\)	67,032
4	26	25	876,204	\(279241/46116\)	22,781,304
5	51	49	570,408,804	\(361136941/30021516\)	28,520,440,200
6	100	97	1,398,071,978,604	\(1767097332025/73582735716\)	137,011,053,903,192