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
The sequence f is strongly complete, and this is proved in [Gr64d].
IsAddStronglyCompleteNatSeq Erdos346.fSolvedStatement only, no proof