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
Erdős and Graham [ErGr80] remark that it is easy to see that if A (n + 1) / A n > (1 + √5) / 2 then the second property is automatically satisfied.
∀ {A : ℕ → ℕ}, (∀ (n : ℕ), (1 + √5) / 2 * ↑(A n) < ↑(A (n + 1))) → ∀ {B : Set ℕ}, B ⊆ Set.range A → B.Infinite → ¬IsAddComplete (Set.range A \ B)SolvedStatement only, no proof