Erdős problem 600
Let . Is it true that as ?
Sources
FormalConjectures/ErdosProblems/
600.lean
Retained formal statement
Let . Is it true that as ?
True ↔ ∀ (r : ℕ), 2 ≤ r → Filter.Tendsto (fun n => ↑(Erdos600.eFunction n (r + 1)) - ↑(Erdos600.eFunction n r)) Filter.atTop Filter.atTopOpenStatement only, no proof