A prime in every short interval above 1.1 * 10^10 (Ramare-Saouter)

Open

TaoFivePrimes.prime_in_short_interval

by Jack McCarthy · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorynumerical-verificationprime-gaps

For every real $x \ge 1.1 \times 10^{10}$ there is a prime $p \le x$ with $x - p \le x/(2.8 \times 10^7)$ ; that is, the interval $[x(1 - 1/(2.8\times10^7)),\, x]$ always contains a prime.

This is Theorem 8.1 of Tao's paper, quoted from Ramar'e and Saouter. Combined with the Goldbach verification (Theorem 1.6) it settles the five-prime claim for all odd numbers up to $(2.8 \times 10^7)^3 N_0 \ge 8.7 \times 10^{36}$ , which is what reduces the main theorem to the range handled by the circle method.

The Ramar'e-Saouter proof itself depends on the numerical verification of the Riemann hypothesis recorded in Theorem 1.5, so this milestone is not independent of it.

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem prime_in_short_interval (x : ℝ) (hx : 1.1 * 10 ^ 10 ≤ x) :
    ∃ p : ℕ, p.Prime ∧ (p : ℝ) ≤ x ∧ x - p ≤ x / (2.8 * 10 ^ 7) := by
  sorry

end TaoFivePrimes

Source

Terence Tao, https://arxiv.org/abs/1201.6656, Theorem 8.1 (p. 36); originally O. Ramare and Y. Saouter, Short effective intervals containing primes, J. Number Theory 98 (2003), 10-33, Theorem 3

Read-back

What the Lean code literally says, in plain math · claude-opus-5

The statement fixes one explicit real variable $x$ , subject to the single hypothesis

1.1 \cdot 10^{10} \;\le\; x,

where the left-hand side is the real number $1.1 \times 10^{10} = 11{,}000{,}000{,}000$ (a real numeric literal $1.1$ multiplied by the real power $10^{10}$ ). There are no other hypotheses, no implicit arguments, and no typeclass assumptions. The hypothesis is satisfiable — every real $x \ge 1.1\times10^{10}$ meets it — so the claim is not vacuous, and note that $x$ ranges over all such reals, not merely integers; $x$ is bounded below but not above.

Under that hypothesis the claim is a plain existence assertion (existence only, not uniqueness): there exists a natural number $p$ such that all three of the following hold simultaneously.

$p$ is prime in the sense of $\mathbb{N}$ (so in particular $p \ge 2$ , ruling out $p = 0$ and $p = 1$ ).
Viewing $p$ as a real number via the canonical cast $\mathbb{N} \to \mathbb{R}$ , $p \le x$ , a non-strict inequality, so $p = x$ is permitted when $x$ happens to be a prime integer.
The gap between $x$ and $p$ , computed as real subtraction (not truncated natural subtraction, so it may in principle be negative, though the previous item forces it to be $\ge 0$ ), satisfies

x - p \;\le\; \frac{x}{2.8 \cdot 10^{7}},

again non-strict, where the denominator is the real number $2.8 \times 10^{7} = 28{,}000{,}000$ . This is ordinary real division by a nonzero constant, so no division-by-zero junk value arises.

Combining the last two items, the two inequalities together say exactly that $p$ lies in the closed real interval

\left[\,x - \frac{x}{2.8\cdot 10^{7}},\; x\,\right] \;=\; \left[\,x\left(1 - \tfrac{1}{2.8\cdot 10^{7}}\right),\; x\,\right],

an interval of length $x/(2.8\times 10^{7})$ , which under the hypothesis is at least $11{,}000{,}000{,}000 / 28{,}000{,}000 \approx 392.86$ and grows proportionally with $x$ . Nothing asserts that $p$ is the largest prime not exceeding $x$ , that $p$ is unique, that there is more than one such prime, or anything about primes above $x$ ; the assertion is only that at least one prime falls in that interval below $x$ . The bound is relative (a fixed fraction $1/(2.8\times 10^7)$ of $x$ ) rather than an absolute gap, and the statement is a single implication from the lower bound on $x$ to that existence claim, with no converse direction claimed.

Human review

Endorsed by marwahaha · Sep 7, 2026
Endorsed by Jack McCarthy · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph