Is there an infinite Sidon set $A \subset N$ such that $∣ A \cap {1 \dots, N}∣ ≫_{ϵ} N^{1/2 - ϵ}$ for all $ϵ > 0$ ?

unreviewedOpen. Best to date: honest null, not yet machine-sealed.

number theory · open · prize $500 · formalized (Lean) · 1 attempt

machinery: Sidon/B_h,additive-combinatorics,greedy/probabilistic-construction,B_h-set-growth,number-field-construction

Check This Result Yourself

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence1

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.

unverified AI candidates (2)

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

This is **open** (it’s one of Erdős’s longstanding problems on infinite Sidon sequences).

candidate solution ↗

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

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

candidate solution ↗

Formal proof

AMS 11 · open (literature)

theorem erdos_39 : answer(sorry) ↔ ∃ (A : Set ℕ), A.Infinite ∧ IsSidon A ∧
    ∀ᵉ  (ε  > (0 : ℝ)),
    (· ^ (1 / 2 - ε) : ℕ → ℝ) =O[atTop] fun N => (((Set.Icc 1 N) ∩ A).ncard : ℝ)

formal-conjectures/39.lean ↗

Connections1

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

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela