Let $A$ be a finite Sidon set and $A + A = {s_{1} < \dots < s_{t}}$ . Is it true that $\frac{1}{t} 1 \leq i < t \sum (s_{i + 1} - s_{i})^{2} \to \infty$ as $∣ A ∣ \to \infty$ ?

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

sidon sets · 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

This exact question is (as far as I can find) **still open**.

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_153 : answer(sorry) ↔ Tendsto f atTop atTop

formal-conjectures/153.lean ↗

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

open

evidence

formal

links

status

Search Vela