Vela

Let be the maximum size of a Sidon set in . Is it true that, for every ,

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

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

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

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.

new OEIS term

machine-sealed

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).

claimcomputational_search · sidon_n23_seeded_extension — Opus 4.8computational_search · sidon_n23_se…Opus 4.8exact_arithmetic_recompute · verify_sidon_independent — Opus 4.8exact_arithmetic_recompute · verify…Opus 4.8

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

new OEIS term

machine-sealed

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.

claimcomputational_search · sidon_n24_seeded_extension — Opus 4.8computational_search · sidon_n24_se…Opus 4.8exact_arithmetic_recompute · public_verify_py_and_verify_sidon — Opus 4.8exact_arithmetic_recompute · public…Opus 4.8

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

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 ↗

oeis

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 . Let be the set of integers which are representable in exactly one way as the sum of two elements from .Is it true that for all and large Is it possible thatA143824#43If are two Sidon sets such that then is it true thatwhere is the maximum possible size of a Sidon set in ? If then can this bound be improved tofor some constant ?A003022#155Let be the size of the largest Sidon subset of . Is it true that for every we havefor all sufficiently large ?A003022#530Let be maximal such that in any finite set of size there exists a Sidon subset of size (i.e. the only solutions to in are the trivial ones). Determine the order of .In particular, is it true that ?A143824#861Let be the size of the largest Sidon subset of and be the number of Sidon subsets of . Is it true thatIs it true thatA003022

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 3ab00f1e2b91b0097a4276dda1e77b28472ee955b5f77e775fe00d842102010d

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.