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 ievery 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 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. [d: direct live-page observation] | Live field | Value on 2026-07-27 | |---|---:| | Status | | 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. [d: direct discussion-page observation] 1. 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\). 2. MalekZ, 8 May: asks which harness was used. 3. Lech Mazur, 9 May: describes the harness. 4. MalekZ, 11 May: brief harness follow-up. 5. 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. 6. Lech Mazur, 9 May: reports that the Lean statement and proof were updated to include the all-index pointwise bound. 7. 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: [d: bibliographic verification] The site's 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. [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 I inspected the theorem on printed page 65 of the primary The exact inspected file has SHA-256 [a, from that theorem] Since 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. [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 This was read directly from printed page 142 of the primary The inspected file has SHA-256 [a, from that theorem] Applying the finite bound to \(\{a_1,\ldots,a_n\}\subset[1,a_n]\) yields 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. [d: fresh machine audit] I cloned the repository at commit 4.30.0-rc2/mathlib build: All 8,335 build jobs completed successfully. Both placeholder scans reported no identical public statement from the checked library. I did not rerun the repository's optional external comparator. [b: named checked theorem] 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 [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. Fix a finite prefix \(A_0\subset[1,M_1)\). For arbitrary positive integers \(k_j\), defineStop-condition audit
OPEN |All seven comments
Literature and artifact audit
Original source
[Er98] is:Erdős–Nicolas–Sárközy (1991)
176829aac870e1a120fa4f547d32b575f09a664a3f0a74d3dec32c0eaa9bc81c.Deshouillers–Freiman (1999)
b376104edc3ba632f15b490d75de53b38dfd0b801dc143c24702d638435b29da.May 2026 carry construction
d450886bd73e7a188b8b8bbe7b9aec771d3b06a1 and ran its pinned Leanlake exe cache get
lake build AdmissibleCarry Challenge Solution
bash scripts/audit_sorries.sh .
bash tools/check_no_sorry.sh
bash scripts/audit_imports.sh .
sorry, admit, axiom, or unsafe occurrence in the proof library.Challenge.lean itself intentionally contains the trusted statement as asorry, and the build reports that warning; Solution.lean proves theAdmissibleCarry.published_final_construction states an infinite admissibleSearch miss
New result: schedule-optimality of the posted carry blocks
Framework
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 \(O(\log h_{j-1})\). Blocks are globally ordered becauseProof, part 2: convert the actual gaps to a control recurrence
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\(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 (13) has the positive minimum The cost bound also gives \(0 at every sufficiently large stage. This forces \(t_j\to\infty\), while \(2t_j+r_j\le C\) forces \(t_j 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. [a: elementary-rigorous algebra] Equality is the stationary control: [b: checked posted theorem] The schedule in the May 2026 artifact attains the endpoint, with both and Together with (1), this classifies the coefficient-one exponents obtainable by this exact carry-block/closure framework: The standalone checker is It uses only the Python standard library. Run: The first command took 6.21 seconds and 22,408 KB maximum RSS on this VM. [d: computational-only] 1. All quadratic-surd identities, including \((5-2\sqrt6)^{-1}=5+2\sqrt6\) and the barrier root. 2. 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. 3. 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. 4. 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 | 5. 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\). 6. With 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. [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: force \(k_{j+1}-1\ge2(k_j-1)\); or \(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: 1. cardinality-graded subset-sum differences; 2. the first element and all early consecutive gaps; 3. the next modulus/scale; and 4. 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 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. [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.Sharpness inside the framework
Independent checker and exact finite audit
runs/erdos875_wave7q_reverify.py (SHA-256413025a74d6810cc28c91b3df936c57c04d24d9c6c4b7efebf915278de87ba33).python runs/erdos875_wave7q_reverify.py
python runs/erdos875_wave7q_reverify.py \
--max-local-k 8 --schedule-stages 4 --check-sources
What is recomputed
--check-sources, fresh downloads of the two primary PDFs and theirExact remaining wall
Honest scope