Erdős problem 893
Does the limit tend to infinity?
Sources
FormalConjectures/ErdosProblems/
893.lean
Retained formal statement
Does the limit tend to infinity?
(Other finite limits have been ruled out by [KoLu25], see below)
True ↔ Filter.Tendsto (fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n)) Filter.atTop Filter.atTopOpenStatement only, no proof