Vela

With and let for be the least integer which can be expressed uniquely as for .What can be said about this sequence? Do infinitely many pairs occur? Does this sequence eventually have periodic differences? Is the density ?

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

number theory · 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=none) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'none'. 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 the **classical Ulam sequence** [[nomath]](the $(1,2)$-Ulam numbers)[[/nomath]], OEIS **A002858**. It begins [ 1,2,3,4,6,8,11,13,16,18,26,28,\dots ] and is defined exactly as you wrote: each new term is the smallest integer larger than the previous term that has **exactly one** representation as a sum of two **…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 5 11 40 · test (literature)

theorem erdos_342.test.a0 : ∀ a : ℕ → ℕ, IsUlamSequence a → a 0 = 1
formal-conjectures/342.lean ↗

oeis

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 85d22987443960cc2d004f516f9c4f2717fa58310994f4dcf9ef0f358c67a96b

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.