Erdős Problem 454

References:

• erdosproblems.com/454
• [Po79] Pomerance, Carl, The prime number graph. Math. Comp. (1979), 399-408.

noncomputable def Erdos454.f (n : ℕ) : ℕ

Define f n to be the minimum of (n + i).nth Prime + (n - i).nth Prime over 0 < i < n.

Equations

• Erdos454.f n = if n ≤ 1 then 0 else ⨅ (i : { i : Fin n // 0 < ↑i }), Nat.nth Prime (n + ↑↑i) + Nat.nth Prime (n - ↑↑i)

theorem Erdos454.erdos_454 : sorry ↔ Filter.limsup (fun (n : ℕ) => ↑(f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

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

theorem Erdos454.erdos_454.two_le_limsup : 2 ≤ Filter.limsup (fun (n : ℕ) => ↑(f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop

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