Let $A = {1, 2, 4, 8, 13, 21, 31, 45, 66, 81, 97, \dots}$ be the greedy Sidon sequence: we begin with $1$ and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to $a + b = c + d$ ). What is the order of growth of $A$ ? Is it true that $∣ A \cap {1, \dots, N}∣ ≫ N^{1/2 - ϵ}$ for all $ϵ > 0$ and large $N$ ?

Open — best to date is a honest null, not yet sealed.

number theory · open · formalized (Lean) · 1 attempt

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.

unverified AI candidates (2)

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

Write the greedy Sidon set as (A={a_1<a_2<a_3<\cdots}) (this is the **Mian–Chowla sequence**), and let [ A(N):=\lvert A\cap{1,\dots,N}\rvert. ]

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 5 · test (literature)

theorem greedySidon_go_singleton_two : (greedySidon.go {1} (by simp [IsSidon]) 2).val = 2

formal-conjectures/340.lean ↗

oeis

A005282 — Mian-Chowla sequence (a B_2 sequence): a(1) = 1; for n>1, a(n) = smallest number > a(n-1) such that the pairwise sums of elements are all distinct.1,2,4,8,13,21,31,45,66,81,97,123,148,182,204,252,290,361,401,475,565,593,662,775,822,916,970,1016,1159,1312,1395,1523,15 A080200 — Numbers that do not occur as differences between terms of the Mian-Chowla sequence A005282.33,88,98,99,105,106,112,126,130,132,134,150,152,154,156,162,163,165,170,176,184,188,198,205,214,215,217,220,222,228,234,

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

status