Erdős problem 295
Let denote the smallest such that there exists with
Sources
FormalConjectures/ErdosProblems/
295.lean
Retained formal statement
Let denote the smallest such that there exists with
Is it true that ?
sorry ↔ Filter.Tendsto (fun N => ↑(Erdos295.k N) - (Real.exp 1 - 1) * ↑N) Filter.atTop Filter.atTopOpenStatement only, no proof