Riemann hypothesis

Very hard

riemann-hypothesis

Statement

Let

\zeta(s) = \sum_{n=1}^{\infty} n^{-s}

for

\operatorname{Re}(s) > 1

, extended by analytic continuation to a meromorphic function on

\mathbb{C}

with a single simple pole at

s = 1

. The trivial zeros are the negative even integers

s = -2, -4, -6, \ldots

Conjecture (Riemann, 1859): every nontrivial zero of

\zeta(s)

satisfies

\operatorname{Re}(s) = \tfrac{1}{2}

. Task: prove the conjecture, or exhibit a nontrivial zero with

\operatorname{Re}(s) \neq \tfrac{1}{2}

Current frontier

Clay Mathematics Institute Millennium Prize problem ($1,000,000), open since 1859. More than 41% (five-twelfths) of the nontrivial zeros are proven to lie on the critical line (Pratt–Robles–Zaharescu–Zeindler 2020, building on Levinson 1974 and Conrey 1989), and the first ~10^13 zeros have been verified on the line (Gourdon 2004) with none off it.

Formal statement (Lean) — pinned & machine-checkable

def RiemannHypothesis : Prop :=
  ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2

Theorem name: RiemannHypothesis
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/leanprover-community/mathlib4/blob/a3a10db0e9d66acbebf76c5e6a135066525ac900/Mathlib/NumberTheory/LSeries/RiemannZeta.lean ↗

A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.

When this counts as solved

This is binary. A full solve is a rigorous proof that every nontrivial zero of

\zeta(s)

has real part exactly

\tfrac{1}{2}

, OR an explicit, verifiable nontrivial zero with

\operatorname{Re}(s) \neq \tfrac{1}{2}

(a counterexample). Nothing short of that closes it: raising the proven proportion of on-line zeros above the current 41%, widening the zero-free region, extending numerical verification past

10^{13}

zeros, or proving an equivalent reformulation (the explicit formula, Weil's criterion, RH-conditional theorems) is its own result, not 'RH solved'.

Classification

binary

Mine this problem →