Erdős problem #1194 — wave 8j
Access/check date: 2026-07-28 UTC.
Outcome
The problem remains open. I obtained two pieces of verifiable progress:
- (a) Elementary-rigorous: an exact finite compactness formulation of
pointwise upper envelopes for the representation tops, together with an explicit lemma showing that every finite Golomb-ruler prefix extends to an infinite perfect difference set.
- **(d) Computational-only for optimality; (a) for each displayed
witness:** exact finite tables \[ L_N\quad(1\leq N\leq21),\qquad R_N\quad(1\leq N\leq12), \] defined below. A dependency-free Python verifier exhaustively scans 16,534,766 candidate subsets and rechecks every witness from scratch in about 39 seconds on this VM.
This does not close the asymptotic gap. The currently verified lower frontier is of order \(n^2/\log n\) infinitely often, whereas the cited greedy construction gives \(a_n\ll n^3\).
0. Mandatory live-page gate
I used the Bright Data browser path, not datacenter curl, to read:
- <https://www.erdosproblems.com/1194>
- <https://www.erdosproblems.com/latex/1194>
- <https://www.erdosproblems.com/forum/discuss/1194>
Live status and markers
(d: browser observation) The page displayed OPEN, `0 claimed proofs for this problem, and Currently working on this problem None`. It also displayed Interested in collaborating None. Therefore the requested stop condition was not triggered. The problem page said it was last edited 24 April 2026; the discussion had eight comments, the newest dated 3 May 2026.
Verbatim current statement
Let \(A\subset\mathbb{N}\) be such that every integer \(n\geq 1\) can be written uniquely as \(a_n-b_n\) for some \(a_n,b_n\in A\). How fast must \(a_n/n\) increase?
This is copied from the page's current LaTeX source. Here \(a_n\) is the larger endpoint in the representation of the difference \(n\), not the \(n\)-th element of \(A\). One page comment initially made exactly this misreading and then explicitly retracted it.
Results listed on the live problem page
The page lists the following. This subsection records the page, rather than silently treating every sentence as independently proved.
- (b, modulo the cited construction [Le04]): perfect difference sets exist,
and the greedy construction achieves \(a_n\ll n^3\).
- (b, modulo Erdős's Sidon-set theorem as cited through [HaRo66]):
Erdős wrote that \[ \limsup_{n\to\infty}\frac{a_n}{n}=\infty, \] and the density argument on the page gives \(a_n\gg n\log n\) for infinitely many \(n\).
- (b, modulo [CiNa08]): Cilleruelo and Nathanson transfer density results
from Sidon sets to perfect difference sets.
- (c as printed; internally contradicted by the comments): the page says
that a GPT-5.4 Pro argument gives \(a_n\gg n^{2-o(1)}\) infinitely often and, more specifically, \(a_n\gg n^2/f(n)\) infinitely often when \(\sum_n1/(nf(n))\) diverges. Two comments explicitly correct “diverges” to “converges”. I do not use the inconsistent printed version as a theorem.
All eight comments read
(d: browser transcription; mathematical statuses noted separately)
- Lech Mazur, 2 May 2026, posted the bound
\[ \lambda=\frac1{2\log2},\qquad B_1=\frac12+\gamma-\log(\log2), \] and, for each fixed \(B>B_1\), arbitrarily large \(n\) with \[ a_n>\lambda\frac{n^2}{\log n-\log\log n+B}. \] The comment linked a Lean repository, a proof sketch, and a detailed proof.
- Nat Sothanaphan, 3 May 2026, reported one possible minor prose issue from a
standard check but said the Lean development appeared to formalize the result correctly. The comment noted that a shorter \(a_n\gg n^2/\log n\) proof might be extractable and described this as overcoming the earlier convergent-sum bound.
- Liam Price, 23 April 2026, said he expected the partial result might be
known and linked a GPT-5.4 Pro partial solution.
- Thomas Bloom, 23 April 2026, first described an \(n^{3/2}\) argument, then
briefly claimed a trivial quadratic bound after confusing \(a_n\) with the \(n\)-th member of \(A\), and finally retracted that claim. The retained recurrence/counting argument balances at exponent \(3/2\).
- Thomas Bloom, later 23 April 2026, distilled an argument ruling out a
uniform \(a_n\ll n^c\) for every \(c<2\), and edited the summability condition to “converges”.
- Nat Sothanaphan, 24 April 2026, explicitly wrote that “diverges” should be
“converges”.
- Thomas Bloom, 24 April 2026, acknowledged and made that correction.
- Nat Sothanaphan, 24 April 2026, reported that a standard check found no
issue in the then-current argument and did not locate it in the literature.
No comment was marked as a claimed proof of the open-ended problem, and no user was marked as currently working on it.
1. Primary-source and artifact checks
Original source
(d: document check) I downloaded Erdős's original paper from the Rényi archive:
P. Erdős, A survey of problems in combinatorial number theory, Annals of Discrete Mathematics 6 (1980), 89–115, <https://users.renyi.hu/~p_erdos/1980-03.pdf>.
The scan's page 100 says that it is easy to construct a sequence in which every integer has a unique difference representation, states the unbounded limsup, and says Erdős could not determine how fast it must increase. The downloaded PDF had SHA-256 e2280c6cbba6bfecedb5c5134ce827c59695dccd7f3377d42658cbc30b8db3cf.
Lev 2004
(b, modulo the published paper; d for bibliographic verification) I downloaded:
V. F. Lev, Reconstructing integer sets from their representation functions, Electronic Journal of Combinatorics 11 (2004), R78, <https://doi.org/10.37236/1831>.
Its Section 3 gives the one-set construction: at a stage, take the least missing difference \(d_n\), adjoin \(z_n,z_n+d_n\), and avoid the finitely many choices that would repeat a difference. It records \(O(n^3)\) excluded choices, \(d_n=O(n^2)\), an \(O(n^3)\) size bound for the newly adjoined elements, and \(A(x)\gg x^{1/3}\). The downloaded PDF had SHA-256 eb3461c80952dd5de69e0a77a680f5af6406c94c36ae40b0a8dda462c3bca6a6.
Cilleruelo–Nathanson 2008
(b, modulo the published theorem; d for bibliographic verification)
J. Cilleruelo and M. B. Nathanson, Perfect difference sets constructed from Sidon sets, Combinatorica 28 (2008), 401–414, <https://arxiv.org/abs/math/0609244>, DOI <https://doi.org/10.1007/s00493-008-2339-4>.
Theorem 1 constructs a perfect difference set whose counting function stays close to that of a prescribed Sidon set (with the paper's factor \(1/3\)). Most directly relevant here, Section 4.1 defines the unique top sequence and asks whether some perfect difference set has \(t_n=o(n^3)\); it says their dense-set method gives a very poor upper bound for \(t_n\). Thus density of \(A(x)\) is not itself control of the endpoint representing a specified difference.
A newer density paper
(b, modulo the publisher's stated Theorem 1.1; d for bibliographic verification) I also found a newer primary source not yet listed on the live page:
Y.-G. Chen and J.-H. Fang, Dense perfect difference sets constructed from Sidon sets, Journal of Combinatorial Theory, Series A 225 (online 2026, volume dated January 2027), article 106239, <https://doi.org/10.1016/j.jcta.2026.106239>.
Its stated theorem improves the density-transfer factor from \(1/3\) to \(1/2\):
(a) This counting-function statement alone does not bound which elements form the unique pair for an individual difference \(n\), so it does not by itself improve the cubic top bound.
The May 2026 lower-bound artifact
(b, rigorous modulo the Lean 4 kernel and pinned mathlib; not a new result of this run) I cloned <https://github.com/lechmazur/erdos_1194> at commit ea9819d2d7027d04481aa27fb7f7bf6322155ceb. I checked that:
Challenge.leanstates the same unique-positive-difference hypothesis and
the two bounds quoted in the comment;
bash tools/check_no_sorry.shfound nosorry,admit,axiom, or
unsafe declaration in the proof library;
lake exe cache get && lake build FloorSavingsucceeded under
leanprover/lean4:v4.30.0-rc2 (8328 build jobs);
#print axiomsreports onlypropext,Classical.choice, andQuot.sound
for both final theorems.
The separate comparator executable was not installed here, so I did not repeat the repository's comparator run. Direct kernel compilation of the proof library did succeed. The checked theorem gives
Numerically, independently recomputed,
Literature-search miss
(c, deliberately not a theorem) Exact-title, exact-phrase, arXiv, and publisher searches located the sources above, but I did not locate a published paper improving the \(n^3\) top upper bound or the May 2026 formal lower bound. This is a search report, not a claim that no such paper exists.
2. An elementary extension lemma
Write
A finite set \(S\) is a Golomb ruler (equivalently, a finite Sidon set in the difference convention) if every member of \(\Delta^+(S)\) has one representation.
Lemma
(a) Elementary-rigorous. Every nonempty finite Golomb ruler \(S\subset\mathbb N\) is contained in an infinite perfect difference set.
Proof
Suppose \(S\) is finite and Sidon. Let \(d\) be the least positive integer missing from \(\Delta^+(S)\), let
(take \(D=0\) when necessary), and choose
Adjoin \(z\) and \(z+d\).
The new positive differences are:
- \(d=(z+d)-z\);
- \(z-s\) for \(s\in S\);
- \(z+d-s\) for \(s\in S\).
All differences in the last two families exceed both \(D\) and \(d\), so none collides with an old difference or with \(d\). Each family has no internal collision. A cross-family collision
would imply \(t-s=d\), contrary to the choice of \(d\). Therefore the enlarged set is still Sidon and now represents \(d\).
Repeat with the new least missing positive difference. Those least missing differences strictly increase, so their union covers every positive integer. Any repeated difference in the union would already occur at a finite stage, where Sidonicity forbids it. The union is the required perfect difference set.
\(\square\)
The verifier also performs 25 iterations of this explicit rule and recomputes all pairwise differences after every iteration. That test is supplementary; the induction above is the proof.
3. Exact finite reductions
Every perfect difference set can be translated so that its least element is \(1\); translation preserves all differences and only decreases its tops. Let \(\mathcal P_1\) denote the normalized perfect difference sets with \(\min A=1\).
Minimum simultaneous top
Define
(a) Elementary-rigorous reduction. \(L_N\) is exactly the least possible length of a finite Golomb ruler \(B\subset\mathbb Z_{\geq0}\) such that
Indeed, from \(A\) take the finitely many endpoints used for differences \(1,\ldots,N\), and translate their minimum to \(0\). The resulting ruler has length at most \(\max_{d\leq N}a_d-1\). Conversely, translate a length-\(L\) ruler to \(B+1\) and apply the extension lemma. Its first \(N\) tops are at most \(L+1\), and their unique representations are preserved. These two inequalities give equality.
Minimum simultaneous ratio
For such a ruler, let \(h_B(d)\) be the larger mark in the unique pair at distance \(d\). Define
(a) Elementary-rigorous reduction. Equivalently,
Translating the finite endpoints extracted from \(A\) down to minimum \(1\) can only decrease all tops, giving one inequality. Extending \(B+1\) gives the reverse inequality. The \(+1\) in the definition is the translation from the zero-normalized ruler \(B\) to the positive set \(B+1\).
A compactness criterion for any proposed envelope
(a) Elementary-rigorous. Let \(F:\mathbb N\to\mathbb N\). There is a normalized perfect difference set with \(a_d\leq F(d)\) for every \(d\) if and only if, for every \(N\), there is a finite Sidon set containing pairs
The forward implication is immediate. For the reverse implication, make a tree whose level-\(N\) nodes are the feasible tuples \(((u_1,v_1),\ldots,(u_N,v_N))\). Each coordinate has finitely many choices, the tree is prefix-closed, and every level is nonempty. König's infinity lemma gives an infinite path. The union of its endpoints represents every positive difference; it is Sidon because any hypothetical repeated difference uses four endpoints and would already violate a finite-level constraint. Finally translate its least element to \(1\), if necessary; this only decreases the tops and preserves every difference.
(b, modulo Erdős's unbounded-limsup result) It follows that \(R_N\) is unbounded: if \(R_N\leq C\) for every \(N\), the criterion with \(F(d)=\lfloor Cd\rfloor\) would produce a perfect difference set satisfying \(a_d/d\leq C\) for all \(d\).
This criterion isolates the remaining construction problem exactly. A proposed uniform upper envelope is valid precisely when all of these finite, bounded feasibility instances have solutions.
4. Exact computation
Exhaustiveness argument
(a) Elementary-rigorous description of the search space. Normalize a finite ruler of length \(L\) to contain \(0\) and \(L\). If it has \(k\) marks, then its \(\binom{k}{2}\) distinct positive differences all lie in \(\{1,\ldots,L\}\), so
The program therefore enumerates, for every \(1\leq L\leq36\), every \((k-2)\)-subset of \(\{1,\ldots,L-1\}\) for all allowable \(k\), adjoining \(0,L\). It rejects a set immediately when a difference repeats. Reflection symmetry is deliberately not removed.
For \(L_N\), the first feasible length proves the upper bound and exhaustion of all shorter lengths proves the lower bound.
For \(R_N\), unused marks may be deleted and the remaining ruler translated back to minimum \(0\), without increasing its score. Its largest mark must be the top of one of the represented differences \(d\leq N\). Thus a competitor of score at most \(C\) has
For the displayed candidate scores and \(N\leq12\), this gives \(\max B\leq36\). Hence the same scan is exhaustive for the ratio table.
Exact \(L_N\) and \(T_N\)
(d) Computational-only for the lower/optimality claims. (a) Each upper bound is directly certified by its witness.
In the table, a witness is the zero-normalized finite ruler \(B\); the corresponding positive prefix is \(B+1\).
| \(N\) | exact \(L_N\) | exact \(T_N=L_N+1\) | witness \(B\) |
|---|---|---|---|
| 1 | 1 | 2 | \((0,1)\) |
| 2–3 | 3 | 4 | \((0,1,3)\) |
| 4–6 | 6 | 7 | \((0,1,4,6)\) |
| 7–9 | 11 | 12 | \((0,2,7,8,11)\) |
| 10–13 | 17 | 18 | \((0,1,4,10,12,17)\) |
| 14–15 | 26 | 27 | \((0,1,7,9,12,22,26)\) |
| 16–18 | 31 | 32 | \((0,5,7,13,16,17,31)\) |
| 19–21 | 35 | 36 | \((0,4,5,17,19,25,28,35)\) |
Expanded:
Exact \(R_N\)
(d) Computational-only for the lower/optimality claims. (a) Each upper bound is directly certified by its witness.
| \(N\) | exact \(R_N\) | one witness covering through \(N\) |
|---|---|---|
| 1–4 | \(2\) | \((0,1,3,7)\) (use its appropriate prefix for smaller \(N\)) |
| 5–7 | \(13/5\) | \((0,1,3,7,12)\) |
| 8–9 | \(21/8\) | \((0,1,3,7,12,20)\) |
| 10–12 | \(31/10\) | \((0,1,3,7,12,20,30)\) |
Expanded:
No value of \(R_{13}\) is claimed. The last witness happens to cover farther, but the \(L\leq36\) cutoff is not sufficient to certify ratio-optimality at \(N=13\).
5. Reproduction and code
The standalone verifier is:
runs/erdos1194_wave8j_verify.py
SHA-256:
363b627d26977e41372f0d9ee7c50d1305c88a5c129d87cd0b31f9b6a5f5f461
Run from the repository root:
python runs/erdos1194_wave8j_verify.py
Environment used: CPython 3.12.3. The complete run printed:
scanned L=36: candidates=16,534,766, Golomb=115,960, elapsed=38.9s
Exact minimum ruler lengths L_N:
1:1 2:3 3:3 4:6 5:6 6:6 7:11 8:11 9:11 10:17 11:17 12:17
13:17 14:26 15:26 16:31 17:31 18:31 19:35 20:35 21:35
Exact normalized minimax ratios R_N:
1:2 2:2 3:2 4:2 5:13/5 6:13/5 7:13/5 8:21/8 9:21/8
10:31/10 11:31/10 12:31/10
enumeration totals: 16,534,766 candidate subsets; 115,960 Golomb rulers
remote-pair extension arithmetic (25 steps): PASS
ALL CHECKS PASSED
The core exhaustive loop is:
for length in range(1, 37):
max_marks = 1
while comb(max_marks + 1, 2) <= length:
max_marks += 1
for mark_count in range(2, max_marks + 1):
for middle in combinations(range(1, length), mark_count - 2):
marks = (0, *middle, length)
seen = 0
is_golomb = True
for high_index, high in enumerate(marks):
for low in marks[:high_index]:
difference = high - low
bit = 1 << difference
if seen & bit:
is_golomb = False
break
seen |= bit
if not is_golomb:
break
if not is_golomb:
continue
The adjacent .py contains the full implementation, direct witness checker, ratio arithmetic using exact fractions.Fraction, all expected-table assertions, enumeration-count assertions, and the extension-step test.
6. What remains and why the standard machinery stalls
- Upper-bound gap. (b, modulo the checked/cited results) The present
range is \[ a_n\gtrsim \frac{n^2}{2\log2\,\log n} \quad\text{infinitely often}, \qquad a_n\ll n^3 \quad\text{for a known construction}. \] The missing object is a construction controlling the specific top \(a_n\), ideally below cubic order. Dense Sidon embeddings control \(A(x)\), but Cilleruelo–Nathanson explicitly note that their method gives poor control of this top sequence.
- Lower-bound frontier. The floor-saving proof exploits integrality in a
weighted top count and reaches the \(n^2/\log n\) scale. (c) I found no justified route in the checked sources from that count to a larger order such as \(n^2\); such a step would require a new loss beyond the current deterministic fractional-part saving.
- Finite-computation wall. (d) The transparent subset enumeration has
8,731,848 candidates at \(L=36\), 19,311,488 at \(L=40\), and jumps to 223,848,241 at \(L=45\) when nine-mark rulers become allowable. At the measured Python rate, length 45 alone is roughly nine minutes; by \(L=55\) the raw count is 6,564,834,826, i.e. several core-hours. Extending the exact table substantially therefore needs a branch-and-bound or SAT model with a checkable UNSAT certificate, not this deliberately simple scanner.
- Uniformity warning. (a) The exact finite tables do not supply one
infinite set realizing all row-wise optima. The minimizing ruler is allowed to change with \(N\). The compactness criterion identifies the required uniform step: for a proposed envelope \(F\), feasible bounded prefixes must exist at every depth so that König's lemma can select a compatible path.
Claim ledger
- (a) Elementary-rigorous: the remote-pair extension lemma; the
ruler/perfect-set equivalences; the envelope compactness criterion; the exhaustiveness bound \(\binom{k}{2}\leq L\); direct validation logic for each witness.
- (b) Rigorous-modulo-named-theorem/artifact: the cited Lev and
Cilleruelo–Nathanson results; the Chen–Fang density theorem; Erdős's unbounded-limsup result; the May 2026 lower bound modulo the successfully built Lean/mathlib proof.
- (c) Plausible/structural-unverified: only the negative literature-search
report and the diagnosis that a genuinely new loss/construction is needed; neither is asserted as a theorem.
- (d) Computational-only: exact optimality in the two finite tables,
enumeration totals and timings, browser status/transcription, document hashes, and build observations.
PARTIAL: Exact finite compactness reduction proved; exhaustive checker certifies \(L_N\) through \(N=21\) and normalized minimax \(R_N\) through \(N=12\); the open asymptotic gap remains \(n^2/\log n\) infinitely often versus a cubic construction.