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

claimed — no verifier run, no signed judgmentunreviewedOpen. Best to date: honest null, not yet machine-sealed.

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

machinery: additive-combinatorics

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

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 proof

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 ↗

Check it yourself

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

vela reproduce examples/erdos-problems

Verify this yourself

Run this command — the output must match these fingerprints.

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

Search Vela

Search problems, results, contributors, and pages — or jump straight to an id.