Erdős problem 346
Let be a set of integers such that is complete for any finite subset and not complete for any infinite subset . If for all , must ? 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.
Sources
FormalConjectures/ErdosProblems/
346.lean
Retained formal statement
Is it true that for every lacunary, strongly complete sequence A that is not complete whenever infinitely many terms are removed from it, lim A (n + 1) / A n = (1 + √5) / 2?
True ↔ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A → (∀ B ⊆ Set.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