Let $F (N)$ be the size of the largest Sidon subset of ${1, \dots, N}$ . Is it true that for every $k \geq 1$ we have $F (N + k) \leq F (N) + 1$ for all sufficiently large $N$ ?

Open problem — our best result is machine-sealed: improved bound, reproduced by an independent verifier. The conjecture itself is unsettled.

additive combinatorics · open · formalized (Lean) · 4 attempts

machinery: Sidon/B_h,extremal-counting-function-continuity,difference-disjoint-perpendicular-sidon-sets,consecutive-integer-window,additive-combinatorics,perfect-difference-set-constructions

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

honest null

needs verification

attempted via frontier 'sidon/B2' (transfer_strength=partial) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'partial'. Do not re-attack cold; needs a new idea or richer accumulated context.

improved bound

machine-sealed

A309370 (max integer-sum Sidon subset of {0,1}^n): NINE verified NEW lower-bound records beating the current OEIS best-known, Opus-independently-verified. Each set is a genuine Sidon set (re-verified from scratch with a base-3 per-bit vector-sum verifier distinct from the search's (a&b,a|b) key; matches OEIS definition 'a+b=c+d trivial only', doubles included; reproduces official a(0..5)=1,2,3,5,7,12). Improvements over the current OEIS comments (incl. Blair Jun 2-3 2026 and Sievers Sep 2025): a(9)>=47 (was 46), a(11)>=92 (was 87), a(12)>=133 (was 120), a(13)>=185 (was 169), a(14)>=257 (was 237), a(15)>=364 (was 334), a(16)>=505 (was 503), a(19)>=1435 (was 1397), a(20)>=1989 (was 1941). These are verified LOWER BOUNDS (A309370 is keyword:hard/more; exact values for n>=7 unknown), to be submitted as OEIS comment updates with witnesses (same format as the existing Blair Link). a(7)=24, a(8)=33, a(17)=712 MATCH current best (not new); a(10)=65 is below the current 66.

Novelty established against the authoritative OEIS A309370 page (read 2026-06-04 via browser-UA curl): base table a(7..18)>=23,32,45,63,87,120,169,237,334,472,662,864; Sievers a(7)>=24; Blair Jun 2 a(16..22)>=503,712,1010,1397,1941,2694,3770; Blair Jun 3 a(8,9,10)>=33,46,66. The big n=11..15 jumps beat the ORIGINAL weak base values (never updated). Witnesses in examples/erdos-problems/attack/sidon-a309370-verified-bounds.v1.json. Submission = comment update + Blair Link extension (Will is the OEIS-authenticated contributor). NOT exact terms (lower bounds only).

Opus base-3 verifier: 9 record sets genuine Sidon at claimed sizes; each > current OEIS best-known; definition matches (a(0..5) reproduced).

obstruction map

machine-sealed

Erdős #155 (F(N+k)<=F(N)+1 eventually <=> g(k):=limsup(F(N+k)-F(N))<=1): the B_2/endpoint route does NOT prove it, Opus-verified. The elementary difference count gives only the Golomb lower bound s(s-1)<=2(L-1), not the sharp Sidon upper bound. The endpoint-deletion reduction gives F(N+k)<=F(N)+h(k), h(k)=max disjoint-difference Sidon-pair size, but h(3)>=2 (X={1,2},Y={1,3} Sidon, (X-X)∩(Y-Y)={0}, verified) so it yields +2 not +1. The clean exact obstruction: #155 <=> optimal Golomb-ruler gap growth G(m+1)-G(m)->infinity; the B_2 count gives no mechanism for gap-growth. Honest obstruction map.

Verified: h(3)>=2 (X={1,2},Y={1,3} disjoint nonzero diffs).

X={1,2},Y={1,3} Sidon with disjoint diffs -> h(3)>=2

superseded (1)

extends prior work

machine-sealed

A309370 (max integer-sum Sidon subset of {0,1}^n): VERIFIED Sidon constructions giving lower bounds a(n) >= size for n=7..20, Opus-independently-verified by two methods. Sizes: a(7)>=24, a(8)>=33, a(9)>=47, a(10)>=65, a(11)>=92, a(12)>=133, a(13)>=185, a(14)>=257, a(15)>=364, a(16)>=505, a(17)>=712, a(19)>=1435, a(20)>=1989. Each set independently re-verified with a from-scratch base-3 per-bit vector-sum verifier (distinct from the workflow's (a&b,a|b) key): all elements distinct and in [0,2^n), all pairwise integer-vector sums distinct (incl. doubles); the verifier agrees with the known a(7)=24. SCOPE/HONESTY: OEIS A309370 officially lists only a(0..6)=1,2,3,5,7,12,15, so these are NOT OEIS terms to 'beat'; NOVELTY vs best-known integer-sum constructions for n>=7 is NOT established (the workflow's reference numbers are of unverified provenance; the F_2^n XOR-Sidon literature table is a DIFFERENT, smaller-valued problem and not comparable). Verified valid lower bounds, NOT claimed records/new terms.

Integer-sum Sidon (B_2) in {0,1}^n (not XOR/F_2^n). 51-agent diverse search. Opus independent base-3 vector-sum verifier over all pairs incl. i==j; 13 sets genuine (artifact examples/erdos-problems/attack/sidon-a309370-verified-bounds.v1.json). Promotion to improved-bound / OEIS submission requires first confirming the current best-known integer-sum values for n>=7 (a real, not-yet-done task). The +38/+48 'beats' at n=19/20 are NOT validated as records.

Opus independent base-3 verifier: 13 sets (n=7..20) genuine Sidon; agrees with a(7)=24. Novelty NOT verified.

superseded: novelty resolved: 9 confirmed new records vs OEIS best-known

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

For (k=1), **yes**, and it is true for **every** $N$ (no “large $N$” needed).

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · open (literature)

theorem erdos_155 : answer(sorry) ↔ ∀ k ≥ 1, ∀ᶠ N in atTop, F (N + k) ≤ F N + 1

formal-conjectures/155.lean ↗

oeis

A003022 — Length of shortest (or optimal) Golomb ruler with n marks.1,3,6,11,17,25,34,44,55,72,85,106,127,151,177,199,216,246,283,333,356,372,425,480,492,553,585 A143824 — Size of the largest subset {x(1),x(2),...,x(k)} of {1,2,...,n} with the property that all differences |x(i)-x(j)| are distinct.0,1,2,2,3,3,3,4,4,4,4,4,5,5,5,5,5,5,6,6,6,6,6,6,6,6,7,7,7,7,7,7,7,7,7,8,8,8,8,8,8,8,8,8,8,9,9,9,9,9,9,9,9,9,9,9,10,10,10 A227590 — a(n) = A003022(n)+1 with a(1)=1.1,2,4,7,12,18,26,35,45,56,73,86,107,128,152,178,200,217,247,284,334,357,373,426,481,493,554,586

links

Vela Sidon frontier (A309370) · verified work

A B₂/Sidon problem — the same object family as Vela's verified Sidon records, where nine improved terms were accepted into OEIS A309370 (the campaign's first external adoption).

OEIS A309370 ↗ · verified-combinatorics (witnesses + verify.py) ↗ · the Erdős campaign

related: #321

#14Let