Erdős problem 454
Is it true that limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/454.leanTrue ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤OpenStatement only, no proof