No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.
theorem riemann_hypothesis :
∀ s : ℂ, riemannZeta s = 0 →
(¬∃ n : ℕ, s = -2 * (↑n + 1)) →
s ≠ 1 →
s.re = 1 / 2 := by
sorryRiemann Hypothesis: All non-trivial zeros of the Riemann zeta function lie on the critical line .
The Riemann zeta function has trivial zeros at and a pole at . The non-trivial zeros (in the strip ) are conjectured to all satisfy .
Proposed by Riemann in 1859. Equivalent to the sharpest prime number theorem error term. One of the seven Millennium Prize Problems ($1M prize). Over zeros verified numerically on the critical line.
No open leaves. Every sub-goal is proved or awaiting decomposition.