Erdős problem 454 · problems.science

Is it true that limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

454.lean

Retained formal statement1 of 2

Is it true that limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤?

FormalConjectures/ErdosProblems/454.leanErdos454.erdos_4541 lineExact file

1True ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

OpenStatement only, no proof