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 statement2 of 2

limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop ≥ 2, and this is proved in [Po79].

FormalConjectures/ErdosProblems/454.leanErdos454.erdos_454.variants.two_le_limsup1 lineExact file

12 ≤ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop

SolvedStatement only, no proof