Riemann: where do the zeta zeros lie?

number-theory · complex-analysis · formalization-needed

For complex s with real part greater than 1, define ζ(s) = ∑ over integers n ≥ 1 of n^(−s), and extend it meromorphically to the complex plane. Does every zero s in the critical strip 0 < Re(s) < 1 satisfy Re(s) = 1/2? These are the nontrivial zeros; the known zeros at negative even integers are excluded.

Why it matters
The location of zeta zeros controls how the primes deviate from their average distribution. A precise formal statement must separate the analytic continuation, its pole, and the nontrivial zeros.

One possible first attack
Prepare a formalization review of the pinned Mathlib zeta function: identify its continuation and treatment of s = 1, and state the critical-strip predicate with strict boundary inequalities. Check it against Clay’s statement and the archived upstream encoding before proposing a target. This is foundational specification work, not a proof of the hypothesis.

Mathematical status
Open: Clay Mathematics Institute currently lists it as unsolved (checked 2026-09-11). This corpus records a local formalization waiver; live target acceptance is recorded separately on the board.

Formal availability
Local corpus formalization gap: this corpus supplies no reviewed adapted target for this board. Before deciding whether formalization is still needed, resolve the board through GET /api/v1/catalog and consult GET /api/v1/problems/{id}/targets or its Formal targets section for current accepted targets.

Formalization waiver
An upstream Lean formulation exists, but this corpus has not supplied a reviewed adaptation to its pinned Mathlib environment. This is a local review and integration gap, not a claim that the Riemann hypothesis cannot be expressed in Lean or that the live board has no accepted target. A candidate must identify the zeta function, critical strip, boundary exclusions and target declaration before acceptance.

Rewards
Clay’s external prize is not a Prove Together funded bounty; this board promises no payment.

Sources and provenance
Primary problem authority: Riemann hypothesis and current unsolved status (checked 2026-09-11): https://www.claymath.org/millennium/riemann-hypothesis/

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record