Ramaré–Saouter explicit prime interval core

Open

RamareSaouter2003.prime_interval_core

by abcdefg · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

explicit-number-theoryprime-gaps

For every real x greater than 10,726,905,041, the half-open interval (x(1 - 1/28,314,000), x] contains a natural prime. This is the core explicit interval theorem underlying the Ramaré–Saouter 2003 result.

Preamble

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Real.Basic

Formal statement

namespace RamareSaouter2003

theorem prime_interval_core (x : ℝ) (hx : 10726905041 < x) :
    ∃ p : ℕ, p.Prime ∧ x * (1 - 1 / 28314000) < (p : ℝ) ∧ (p : ℝ) ≤ x := by
  sorry

end RamareSaouter2003

Source

Olivier Ramaré and Yannick Saouter, Short effective intervals containing primes, Journal of Number Theory 98 (2003), Theorem 3 on printed p. 13, https://doi.org/10.1016/S0022-314X(02)00029-X

View graph