Erdős problem 1191 — wave 8j

Date: 2026-07-28 (UTC)

Claim labels

• [a] elementary-rigorous: proved directly below.
• [b] rigorous-modulo-named-theorem: the deduction uses the explicitly

named primary-source theorem.

• [c] plausible/structural-unverified: a search conclusion, diagnosis,

heuristic result, or engineering estimate; not a theorem.

• [d] computational-only: a finite result certified by the standalone

exhaustive checker in this report.

No claim below says that either question in problem 1191 is solved.

0. Mandatory live-page gate

[a, direct source observation] I fetched the live page <https://www.erdosproblems.com/1191> on 2026-07-28 through the Bright Data browser path and saved a full-page screenshot. The page showed:

• status OPEN — $1000;
• 0 comments;
• 0 claimed proofs;
• “Currently working on this problem: None”;
• “Interested in collaborating: None”;
• all other participation markers as “None”; and
• last edit 06 April 2026.

Thus the mandatory stop condition did not fire.

The following is the statement verbatim from the live page:

Let \(A\subset\mathbb N\) be an infinite Sidon set. Is it true that \[ > \liminf_{x\to\infty} > \frac{\lvert A\cap[1,x]\rvert}{x^{1/2}}(\log x)^{1/2}=0? > \] Does there exist an infinite Sidon set \(A\) such that \[ > \liminf_{x\to\infty} > \frac{\lvert A\cap[1,x]\rvert}{x^{1/2}}(\log x)^c>0 > \] for some \(c>0\)?

[b, as stated on the live page] The page records the known bound

for some absolute \(C>0\), citing Erdős and [HaRo66]. It says that Erdős offered $1000 in [Er80] for “clearing up” the associated questions, that the second question strengthens problem 39, and that problem 729 concerns the limsup.

1. Primary-source and literature audit

Sources actually checked

1. [a, source-verified] Paul Erdős, *A survey of problems in

combinatorial number theory*, Annals of Discrete Mathematics 6 (1980), 89–115, is available in the Erdős archive: <https://users.renyi.hu/~p_erdos/1980-03.pdf>. I downloaded the scan, extracted its text, and visually inspected printed page 98. In its notation \(a_1<a_2<\cdots\), formula (5) is \[ \limsup_{k\to\infty}\frac{a_k}{k^2\log k}>0. \] Erdős immediately asks whether this limsup is infinity, asks whether a \(B_2\)-sequence can satisfy \(a_k<c_1k^2(\log k)^{c_2}\) for all \(k\), and then offers $1000 for the questions raised by (5) and (6). This verifies the live page's provenance.

1. [b, Ruzsa 1998] Imre Z. Ruzsa, “An infinite Sidon sequence,”

Journal of Number Theory 68 (1998), 63–71, <https://doi.org/10.1006/jnth.1997.2192>, constructs an infinite Sidon set with \[ A(x)=x^{\sqrt2-1+o(1)}. \tag{1.1} \]

1. [b, Cilleruelo 2014] Javier Cilleruelo, “Infinite Sidon

sequences,” Advances in Mathematics 255 (2014), 474–486, <https://doi.org/10.1016/j.aim.2014.01.011> (preprint: <https://arxiv.org/abs/1209.0326>), gives an explicit construction with the same exponent \(\sqrt2-1\). Its Theorem 1.2 and proof were checked in the primary preprint. Thus (1.1) is not merely a nonconstructive density record.

1. [b, O'Bryant 2026] Kevin O'Bryant,

“On the Thickness of Infinite Generalized Sidon Sets, I,” <https://arxiv.org/abs/2606.28651>, version 3 dated 26 July 2026, is newer than the live page's last edit. For an infinite \(g\)-Golomb ruler it proves \[ \liminf_{n\to\infty} \frac{A(n)}{\sqrt{n/\log n}} \leq \frac{2\sqrt g}{\sqrt{\log 2}}. \tag{1.2} \] For \(g=1\), this sharpens the known constant in (0.1) to \(2/\sqrt{\log2}=2.4022448175\ldots\), but it does not make that constant zero. Corollary 2 gives \[ \limsup_{n\to\infty}\frac{a_n}{n^2\log n} \geq\frac{\log2}{2g}. \tag{1.3} \] The paper explicitly says that its one-scale energy/Cauchy argument has been fully optimized, while suggesting multiscale, martingale, or entropy information as possible sources of further improvement.

1. [b, Táfula 2026] Christian Táfula,

“Infinite Sidon-type sets for zero-sum linear forms,” <https://arxiv.org/abs/2607.20753>, version 1 dated 22 July 2026, recovers (0.1) in the special vector case \((1,-1)\) while extending the phenomenon to other zero-sum forms. It does not replace the finite right side of (0.1) by zero.

Search result and excluded hit

[c, search-limited] Exact-phrase and formula searches found the live tracker, the primary sources above, surveys, and a ResearchGate upload called Entropy and Arithmetic Progression Methods for Infinite Sidon Sets. The latter displays only an arXiv:submit/... token, not a public arXiv identifier, and its extracted text contains unproved uniformity/diagonalisation steps. I did not treat it as a verified primary source or a claimed solution. The searches found no primary paper proving either assertion on the live page. Search misses are not proof that no such paper exists.

2. Exact sequence and finite-tree reformulation

Write the increasing enumeration of an infinite Sidon set as

Endpoint lemma

[a] Since \(x\mapsto\sqrt{\log x/x}\) is decreasing for \(x>e\), the smallest value on the gap immediately before \(a_{k+1}\) is attained as \(x\) approaches \(a_{k+1}\). Hence

For integer \(x\), use \(x=a_{k+1}-1\); replacing \(a_{k+1}-1\) by \(a_{k+1}\) changes the factor by \(1+o(1)\).

Consequently,

Translation to finite Golomb rulers

[a] Put

The Sidon condition is equivalent to all positive differences \(b_j-b_i\), \(j>i\), being distinct. Thus every prefix

is a normalized finite Golomb ruler, and conversely translating such a ruler gives a finite Sidon set.

For \(d\geq0\), define the exact finite profile

The logarithm is natural. The minimum is attained: any one witness gives a finite upper bound, and beneath that bound every \(b_k\) has only finitely many integer choices.

Log-inversion lemma

[a] Fix \(C>0\) and \(d\geq0\). For integer sequences \(t_k\geq k\), the eventual implicit bound

is equivalent, after changing \(C\), to

Indeed, if (2.4) holds and \(\log t_k>4\log k\), then, for large \(k\), monotonicity of \(e^u/u^d\) gives

a contradiction. Therefore \(\log t_k\leq4\log k\), which gives (2.5). The reverse implication needed here follows from \(\log t_k\geq\log k\) and \(\log(2k)/\log k\to1\).

Compactness proposition

[a] The two live questions are exactly:

1. The answer to the first question is “yes” if and only if

\[ \Lambda_n(1)\longrightarrow\infty. \tag{2.6} \]

1. The answer to the second question is “yes” if and only if there is

some \(d>0\) for which \[ \sup_n\Lambda_n(d)<\infty. \tag{2.7} \] The exponent in the live question is \(c=d/2\).

To prove this, the negation of the first question and (2.1) give \(a_{k+1}\leq Ck^2\log a_{k+1}\) eventually. The log-inversion lemma turns this into a uniform \(k^2\log(2k)\) envelope. Similarly, positivity in the second question is equivalent at gap endpoints to

The log-inversion lemma gives (2.7).

It remains only to justify passage between all finite prefixes and one infinite ruler. Under a fixed envelope, every mark has finitely many choices. If admissible prefixes exist at every depth, choose a first mark occurring in arbitrarily deep prefixes, then a second mark with the same property, and continue. This diagonal infinite-pigeonhole construction produces one infinite path. Conversely, every infinite path supplies all finite prefixes. This proves (2.6) and (2.7) without a hidden uniformity assumption.

This reduction is important: independent dense finite Sidon sets at every scale do not answer the problem unless their constants are uniform and their prefixes are compatible.

3. Exact quadratic-prefix computation

Set

[d] The standalone checker proves the following exact table.

For example, an optimal \(n=21\) witness is

All witnesses for \(13\leq n\leq21\), and a common witness whose prefixes handle \(n\leq12\), are embedded in the verifier.

Why the table is exact

[a, conditional only on exhaustive execution for the UNSAT fact] For a fixed \(n\), the objective of any integer ruler is one of the finite set

below any proposed upper bound. The third column is the largest such value strictly below the claimed optimum. Each listed witness attains the claimed value, while two independent exhaustive searches find no ruler beneath the immediate predecessor. There is no untested real value between the two.

The search is complete by induction on the prefix. Given \((b_0,\ldots,b_{k-1})\), it tries every integer

It accepts \(b_k\) exactly when every new difference \(b_k-b_i\) is absent from the old difference set. One engine stores differences as a Python set; the other stores them as bits of an arbitrary-precision integer. They visit identical node counts but share no state representation.

[d] In particular, \(b_k\leq k^2\) is possible through \(k=12\) but impossible through \(k=13\). This finite statement does not settle an asymptotic question already known to be much weaker than the logarithmic envelope in problem 1191.

4. Directly relevant explicit finite construction

The profile in the first live question is \(\Lambda_n(1)\), not \(\rho_n\). The relevant critical envelope at its unavoidable first-mark floor is

Construction

[d] Start with \(b_0=0\). At every step through \(k=660\), take the least integer larger than the previous mark that repeats no positive difference (the normalized Mian–Chowla greedy rule). At \(k=661\), take the third admissible integer instead of the first. Resume the greedy rule thereafter.

The checker constructs this ruler from scratch. Its relevant values are

It directly checks all \(682\cdot681/2=232\,221\) positive differences in the prefix through \(b_{681}\).

[d] Every prefix through \(k=680\) satisfies (4.1). Numerically, only for orientation,

The next mark of this particular construction fails:

The comparisons in the certificate do not use floating point. For \(1\leq z\leq2\), it encloses

using the exact rational bound

Range reduction then gives rational lower and upper bounds for every \(\log_2(2k)\).

Exact consequence

[a+d] Every normalized ruler has \(b_1\geq1\), so

The construction above attains this bound for every \(n\leq680\): condition (4.1) is exactly

Therefore

The failure at \(k=681\) belongs only to this explicit construction. It is not an exhaustive nonexistence result and gives no upper or lower claim about \(\Lambda_{681}(1)\).

5. Standalone reproduction

The checker is:

runs/erdos1191_wave8j_reverify.py

Run:

python -u runs/erdos1191_wave8j_reverify.py

It uses only the Python standard library. Its final output on this VM was:

n   rho_n       predecessor  set_nodes  bit_nodes
13     145/144      170/169        620        620
14       65/64      199/196        699        699
15       51/49        26/25       2037       2037
16       53/50      179/169       3967       3967
17       52/49        53/50       4198       4198
18     119/108      141/128      27010      27010
19        10/9      401/361      39537      39537
20     451/400      407/361     128630     128630
21     147/128        31/27     350810     350810
rho_1=...=rho_12=1
lambda_1=...=lambda_680=1/log(2)
one-deviation ruler: b_680=4795424 is inside; b_681=4848816 is the first mark of this construction outside b_k <= k^2 log_2(2k)
greedy construction/check time: 51.472 seconds
2/sqrt(log(2))=2.4022448175728996
sqrt(2)-1=0.4142135623730951
ALL CHECKS PASSED in 101.643 seconds

The core append test used by the exhaustive bit engine is:

for x in range(marks[-1] + 1, ceiling + 1):
    fresh_bits = 0
    valid = True
    for y in marks:
        bit = 1 << (x - y)
        if (used_bits | fresh_bits) & bit:
            valid = False
            break
        fresh_bits |= bit
    if valid:
        visit(marks + (x,), used_bits | fresh_bits)

For the long construction, if used_bits represents all old differences, then

forbidden_bits = OR(used_bits << y for y in marks)

has bit \(x\) set exactly when appending \(x\) repeats an old difference. This makes the 681-mark reconstruction practical while retaining exact integer arithmetic.

6. What remains and the precise wall

Upper/zero direction

[b] O'Bryant's (1.2) and (1.3) yield a fixed positive constant. The first question needs the qualitatively stronger conclusion

or, equivalently by Section 2, \(\Lambda_n(1)\to\infty\). Optimizing the weights in the existing one-scale energy argument can improve a constant but cannot by itself create an unbounded factor.

[c, precise missing lemma] A successful upper-bound proof needs cross-scale information ruling out coherent near-extremizers: for every fixed \(C\), it must produce a finite depth \(n(C)\) at which no Golomb ruler can satisfy

The exact computation shows why small cases do not reveal this mechanism: the most directly relevant profile remains at its trivial first-mark floor through \(n=680\).

Construction direction

[b] Inverting Ruzsa's/Cilleruelo's exponent \(\sqrt2-1\) gives

This is still polynomially larger than every \(k^2(\log k)^d\).

[c, precise missing lemma] By (2.7), it would suffice to build compatible finite rulers under one uniform polylogarithmic envelope at every depth. Dense Singer/Bose-type rulers constructed independently at each scale do not provide compatible prefixes: all cross-block differences must also be distinct. What is missing is an extension/pasting lemma that adds a dense next block, destroys only a polylogarithmically controlled number of marks, and keeps the next coordinate within \(Ck^2(\log k)^d\). Present block-union arguments obtain large limsup density only by separating scales too aggressively.

Cost of the next exact computation

[c, engineering estimate] At \(n=681\), the critical envelope allows coordinates near \(4.83\times10^6\), and a candidate has 232,221 distinct positive differences. A heuristic CP/local-search attempt to extend the explicit ruler is plausibly a 1–10 core-hour job. A proof-producing exhaustive UNSAT computation at this scale is a different matter; based on the domain size and all-different constraint, I would budget at least \(10^3\)–\(10^5\) core-hours for an initial distributed CP-SAT/LCG campaign, with no credible upper bound on completion. At a realistic \(\$0.05\)–\(\$0.10\) per core-hour, that is roughly \(\$50\)–\(\$10,000\), before proof-log storage and checking. This is a cost estimate, not a complexity lower bound, and such a finite result would still not supply the uniform asymptotic step.

PARTIAL: reduced both questions to exact monotone finite Golomb-ruler profiles, proved the quadratic profile through n=21, and constructed and exactly verified a critical-log-envelope ruler through n=680; no asymptotic resolution is claimed.