Numerical verification of the even Goldbach conjecture up to 4 * 10^14

Open

TaoFivePrimes.even_goldbach_verified

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

goldbachnumber-theorynumerical-verification

With $N_0 := 4 \times 10^{14}$ , every even number $n$ with $4 \le n \le N_0$ is a sum of two primes.

This is Theorem 1.6 of Tao's paper, quoted from Richstein's 2001 verification. Tao uses it to reduce the five-prime problem to representing $x$ as three primes plus a number below $N_0$ .

The statement is finite and decidable, but it encodes a distributed computation over $2 \times 10^{14}$ cases; it is included so that the mission's dependency graph is truthful, not because a direct proof is within reach of current tooling. Richstein's own verification, and the later one of Oliveira e Silva reaching $2.6 \times 10^{18}$ , were run outside any proof assistant.

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem even_goldbach_verified (n : ℕ) (h4 : 4 ≤ n) (hN : n ≤ 4 * 10 ^ 14) (he : Even n) :
    ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p + q = n := by
  sorry

end TaoFivePrimes

Source

Terence Tao, https://arxiv.org/abs/1201.6656, Theorem 1.6 (p. 7); originally J. Richstein, Verifying the Goldbach conjecture up to 4*10^14, Math. Comp. 70 (2001), 1745-1749

Read-back

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

For every natural number $n$ , if

4 \le n, \qquad n \le 4 \cdot 10^{14} = 400{,}000{,}000{,}000{,}000, \qquad n \text{ is even},

then there exist natural numbers $p$ and $q$ such that $p$ is prime, $q$ is prime, and

p + q = n.

All quantities are natural numbers: $n$ , $p$ , and $q$ range over $\mathbb{N}$ , the bound $4 \cdot 10^{14}$ is a natural-number arithmetic expression evaluated exactly, and $p + q$ is ordinary addition in $\mathbb{N}$ (no subtraction or division occurs, so no truncation or junk-value behaviour is involved). "Even" is the standard notion " $n = r + r$ for some natural number $r$ ", and "prime" is the standard primality predicate on $\mathbb{N}$ , under which $0$ and $1$ are not prime and the smallest prime is $2$ .

Both bounds are inclusive: the hypotheses admit $n = 4$ and $n = 4 \cdot 10^{14}$ themselves, and exclude every even $n$ strictly below $4$ (namely $n = 0$ and $n = 2$ ) and every $n$ strictly above $4 \cdot 10^{14}$ . The three hypotheses are simultaneously satisfiable (for instance by $n = 4$ ), so the statement is not vacuous; nothing beyond these three conditions is assumed about $n$ .

The conclusion asserts bare existence of a pair of primes summing to $n$ . It does not require $p$ and $q$ to be distinct (so $p = q$ is permitted, e.g. $2 + 2 = 4$ ), does not order them ( $p \le q$ is not imposed), does not claim uniqueness of the pair, does not assert that the number of such pairs is positive in any counted sense, and provides no method, algorithm, or bound for producing $p$ and $q$ . It is an existence claim about each individual $n$ in the stated range, not a statement about the range as a whole beyond that.

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