Let $A = {1 \leq a_{1} < a_{2} < \dots}$ be a set of integers such that $A \ B$ is complete for any finite subset $B$ and $A \ B$ is not complete for any infinite subset $B$ . (Here 'complete' means all sufficiently large integers can be written as a sum of distinct members of the sequence.)Is it true that if $a_{n + 1} / a_{n} \geq 1 + ϵ$ for some $ϵ > 0$ and all $n$ then $n lim \frac{a _{n + 1}}{a _{n}} = \frac{1 + 5}{2} ?$

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 'additive-basis' (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 **exactly an Erdős–Graham question**, and as far as the current literature record I can find, it’s **still open**: there is **no known proof** (nor known counterexample) that the extra hypothesis [ \frac{a_{n+1}}{a_n}\ge 1+\varepsilon\quad(\varepsilon>0) ] forces [ \lim_{n\to\infty}\frac{a_{n+1}}{a_n}=\varphi=\…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_346 : answer(sorry) ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A →
    (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) →
    Tendsto (fun n => A (n + 1) / (A n : ℝ)) atTop (𝓝 ((1 + √5) / 2))

formal-conjectures/346.lean ↗

status

open

evidence

formal

status

Search Vela