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

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

\[ \liminf_{x\to\infty} \frac{|A\cap[1,x]|}{x^{1/2}}(\log x)^{1/2}\leq C \tag{0.1} \]

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

\[ \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

the questions raised by (5) and (6). This verifies the live page's

provenance.

2. [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} \]

3. [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.

4. [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.

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

\[ A=\{a_1Endpoint 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

\[ \liminf_{x\to\infty}A(x)\sqrt{\frac{\log x}{x}} = \liminf_{k\to\infty} k\sqrt{\frac{\log a_{k+1}}{a_{k+1}}}. \tag{2.1} \]

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,

\[ \liminf_{x\to\infty}A(x)\sqrt{\frac{\log x}{x}}=0 \quad\Longleftrightarrow\quad \limsup_{k\to\infty} \frac{a_{k+1}}{k^2\log a_{k+1}}=\infty. \tag{2.2} \]

Translation to finite Golomb rulers

[a] Put

\[ b_0=0,\qquad b_k=a_{k+1}-a_1\quad(k\geq1). \]

The Sidon condition is equivalent to all positive differences

$b_j-b_i$, $j>i$, being distinct. Thus every prefix

\[ 0=b_0is a normalized finite Golomb ruler, and conversely translating such a

ruler gives a finite Sidon set.

For $d\geq0$, define the exact finite profile

\[ \Lambda_n(d):= \min_{0=b_0<\cdotsThe 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

\[ t_k\leq Ck^2(\log t_k)^d \tag{2.4} \]

is equivalent, after changing $C$, to

\[ t_k\leq C'k^2(\log(2k))^d. \tag{2.5} \]

Indeed, if (2.4) holds and $\log t_k>4\log k$, then, for large $k$,

monotonicity of $e^u/u^d$ gives

\[ \frac{t_k}{(\log t_k)^d} \geq\frac{k^4}{(4\log k)^d}>Ck^2, \]

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} \]

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

\[ a_{k+1}\leq Ck^2(\log a_{k+1})^{2c}. \]

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

\[ \rho_n:=\Lambda_n(0) =\min_{0=b_0<\cdots[d] The standalone checker proves the following exact table.

|---:|---:|---:|---:|

| $1\leq n\leq12$ | $1$ | — | direct lower bound $b_1\geq1$ |

| 13 | $145/144$ | $170/169$ | 620 |

| 14 | $65/64$ | $199/196$ | 699 |

| 15 | $51/49$ | $26/25$ | 2,037 |

| 16 | $53/50$ | $179/169$ | 3,967 |

| 17 | $52/49$ | $53/50$ | 4,198 |

| 18 | $119/108$ | $141/128$ | 27,010 |

| 19 | $10/9$ | $401/361$ | 39,537 |

| 20 | $451/400$ | $407/361$ | 128,630 |

| 21 | $147/128$ | $31/27$ | 350,810 |

For example, an optimal $n=21$ witness is

\[ \begin{split} (0,1,3,8,12,28,34,51,69,83,98,136,157,176,213,249,\\ \qquad 294,307,359,383,446,500). \end{split} \tag{3.2} \]

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

\[ \left\{\frac{m}{k^2}:1\leq k\leq n,\ m\in\mathbb N\right\} \]

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

\[ b_{k-1}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

\[ b_k\leq k^2\log_2(2k). \tag{4.1} \]

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

\[ b_{661}=4\,466\,351,\qquad b_{680}=4\,795\,424,\qquad b_{681}=4\,848\,816. \tag{4.2} \]

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,

\[ 680^2\log_2(1360)=4\,813\,302.3688\ldots>b_{680}. \]

The next mark of this particular construction fails:

\[ 681^2\log_2(1362)=4\,828\,452.7473\ldotsThe comparisons in the certificate do not use floating point. For

$1\leq z\leq2$, it encloses

\[ \log z =2\sum_{j=0}^{23}\frac{y^{2j+1}}{2j+1}+R,\qquad y=\frac{z-1}{z+1}, \]

using the exact rational bound

\[ 0Range 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

\[ \Lambda_n(1)\geq\frac1{\log2}. \]

The construction above attains this bound for every $n\leq680$:

condition (4.1) is exactly

\[ \frac{b_k}{k^2\log(2k)}\leq\frac1{\log2}. \]

Therefore

\[ \boxed{\Lambda_1(1)=\cdots=\Lambda_{680}(1)=\frac1{\log2}}. \tag{4.3} \]

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

\[ \limsup\frac{a_n}{n^2\log n}=\infty, \]

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

\[ b_k\leq Ck^2\log(2k)\quad(1\leq k\leq n(C)). \]

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

\[ a_k=k^{\,1/(\sqrt2-1)+o(1)} =k^{\sqrt2+1+o(1)} =k^{2.414213\ldots+o(1)}. \]

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.

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