Vela

Let be an infinite set such that the triple sums are all distinct for (aside from the trivial coincidences). Is it true that

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

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

machinery: additive-combinatorics

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

Your condition is exactly what people call a **(B_3)** sequence (a “3‑Sidon set”): all sums $a+b+c$ (with order ignored) are different. Erdős asked this as a specific open problem (it is listed as **open** on the Erdős Problems site). ([Erdős Problems][1])

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

AMS 11 · open (literature)

theorem erdos_41 (A : Set ℕ) (h_triple : NtupleCondition A 3) (h_infinite : A.Infinite) :
    Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ)^(1/3 : ℝ)) = 0
formal-conjectures/41.lean ↗

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

notary

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

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.