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:

1. (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.

2. **(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)

1. 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.

2. 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.

3. Liam Price, 23 April 2026, said he expected the partial result might be

known and linked a GPT-5.4 Pro partial solution.

4. 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\).

5. 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”.

6. Nat Sothanaphan, 24 April 2026, explicitly wrote that “diverges” should be

“converges”.

7. Thomas Bloom, 24 April 2026, acknowledged and made that correction.

8. 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.lean states the same unique-positive-difference hypothesis and

the two bounds quoted in the comment;

• bash tools/check_no_sorry.sh found no sorry, admit, axiom, or

unsafe declaration in the proof library;

• lake exe cache get && lake build FloorSaving succeeded under

leanprover/lean4:v4.30.0-rc2 (8328 build jobs);

• #print axioms reports only propext, Classical.choice, and Quot.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:

1. \(d=(z+d)-z\);

2. \(z-s\) for \(s\in S\);

3. \(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.

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

python runs/erdos1194_wave8j_verify.py

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

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