Skip to content

Erdős problem 346

Let A={1a1<a2<}A=\{1\leq a_1< a_2<\cdots\} be a set of integers such that A\BA\backslash B is complete for any finite subset BB and not complete for any infinite subset BB. If an+1/an1+ϵa_{n+1}/a_n \geq 1+\epsilon for all nn, must limnan+1/an=(1+5)/2\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/346.lean

Formal Conjectures

FormalConjectures/ErdosProblems/346.leanErdos346.erdos_3466 linesExact file
True  ∀ {A : ℕ → ℕ},    IsLacunary A      IsAddStronglyCompleteNatSeq A        (∀ BSet.range A, B.Infinite → ¬IsAddComplete (Set.range A \ B)) →          Filter.Tendsto (fun n => ↑(A (n + 1)) / ↑(A n)) Filter.atTop (nhds ((1 + √5) / 2))
OpenStatement only, no proof

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI collaborating with humans

    Erdős AI contributions wiki · 21 Jun, 2026

    Machine
    Codex, GPT
    People
    Kenta Kitamura
    Open the source record
  • AI alongside literature

    Erdős AI contributions wiki · 19 Jun, 2026

    Machine
    Codex, GPT-5.5 Pro
    Open the source record
  • argument

    VibeMathed

    Machine
    ChatGPT, Codex
    People
    Kenta Kitamura
    Reported outcome
    candidate
    Open the source record

Continue

Search problems.science

Find a Problem, Result, source, or page