Let $h (N)$ be the maximum size of a Sidon set in ${1, \dots, N}$ . Is it true that, for every $ϵ > 0$ , $h (N) = N^{1/2} + O_{ϵ} (N^{ϵ})?$

verifiedThe problem is open. The best result here is machine-verified: new OEIS term, re-checked by an independent verifier.

number theory · open · prize $1000 · formalized (Lean) · 3 attempts

machinery: Sidon/B_h,additive-combinatorics,prime-distribution,extremal-set-system

Check This Result Yourself

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence3

honest null

unverified claim

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.

new OEIS term

machine-verified

OEIS A309370 (max Sidon subset of {0,1}^n) a(23) >= 5179: an independently verified Sidon set of 5179 points in {0,1}^23 (all 13413610 pairwise componentwise sums distinct), extending the sequence to n=23 where no value was recorded. Built by lifting the best n=22 set (3770) into {0,1}^23 and greedily adding new-coordinate vectors; re-checked from scratch by an independent pairwise-sum-distinctness verifier.

scripts/sidon_extend_seeded.py (lift + packed-sum greedy extension); witness at examples/sidon-sets/discoveries/sidon-n23-extension.witness.txt; independent gate verify_construction.verify_sidon recomputes all pairwise sums. The gate caught a stale-membership bug in an earlier incremental check (it rejected the invalid set before any record was written).

python3 -c 'verify_construction.verify_sidon(witness,23)' -> True

new OEIS term

machine-verified

OEIS A309370 (max Sidon subset of {0,1}^n) a(24) >= 7179: an independently verified Sidon set of 7179 points in {0,1}^24 (all 25,772,610 pairwise componentwise sums distinct), extending the sequence to n=24 where no value was recorded. Built by lifting the verified n=23 set (5179) into {0,1}^24 and greedily adding new-coordinate vectors; re-checked from scratch by an independent pairwise-sum-distinctness verifier and by the public Blair-Link verify.py.

scripts/sidon_extend_seeded.py chained from the n=23 witness; public witness at verified-combinatorics/sidon-A309370/sidon_n24_size7179.txt; gate verify_construction.verify_sidon + public verify.py both confirm B_2.

verify_construction.verify_sidon(witness,24)=True; public verify.py: B_2 verified=True (25772610)

unverified AI candidates (2)

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

What is known is that the main term is (\sqrt N), but the best *proved* error term is still of order (N^{1/4}) (up to improving the constant).

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

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

candidate solution ↗

Formal proof

AMS 11 · open (literature)

theorem erdos_30 : answer(sorry) ↔
    ∀ᵉ (ε > 0), (fun N => h N - (N : Real).sqrt) =O[atTop] fun N => (N : ℝ)^(ε : ℝ)

formal-conjectures/30.lean ↗

OEIS3

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

Connections2

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

Green's open problems list · paper

#14Let