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.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/346.leanTrue ↔ ∀ {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
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
AI collaborating with humans
- Machine
- People
AI alongside literature
- Machine
argument
- Machine
- People
- Reported outcome