The board / number theory / #454
Erdős Problem #454
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Define `f n` to be the minimum of `(n + i).nth Prime + (n - i).nth Prime` over `0 < i < n`.
Is it true that `limsup (fun n => (f n - 2 * n.nth Prime : ℕ∞)) atTop = ⊤`?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/454.Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/454
Attempts
submit one →Read our working report →
Reduced the conjecture to a precise growing paired-gap window and certified every prefix record through \(n=10,000,000\), with maximum \(148\) first at \(n=2,886,673\); unboundedness remains open at t
PARTIAL