Problems / riemann-hypothesis / riemann-hypothesis
The **Riemann Hypothesis**
riemann-hypothesis
open
The problem's statement.
theorem Opn.riemannHypothesis :
RiemannHypothesis := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Open. A direct proof closes it.
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and no words yet
Statement not audited — fidelity mechanical-only; QA pass incomplete; no signer yet.
/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Mathlib
/-! The **Riemann Hypothesis**: all non-trivial zeros of the Riemann zeta function have real part $\frac{1}{2}$. — imported from google-deepmind/formal-conjectures (FormalConjectures/Millenium/RiemannHypothesis.lean at c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae, Apache-2.0); stated as the registry states it. Drafted by gate/tools/wave.py (F14-T11) and read by the curator before import (R13). -/
theorem Opn.riemannHypothesis :
RiemannHypothesis := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.
The Riemann Hypothesis: all non-trivial zeros of the Riemann zeta function have real part $\frac{1}{2}$. That is, if $\zeta(s) = 0$, $s \neq 1$, and $s$ is not a trivial zero $-2(n+1)$ for some $n \in \mathbb{N}$, then $\operatorname{Re}(s) = \frac{1}{2}$. This is the official Millennium Prize Problem as posed by the Clay Mathematics Institute. This uses the RiemannHypothesis type from Mathlib, which is defined as ∀ (s : ℂ), riemannZeta s = 0 → (¬∃ n : ℕ, s = -2 * (n + 1)) → s ≠ 1 → s.re = 1 / 2.
Rendered from targets/riemann-hypothesis/nodes/riemann-hypothesis/Statement.lean. Origin: authored.
Witness
Not checked — no run on this page records step 7 passing for it.
32191282b59e./-! Non-vacuity witness (D-4 step 7): the statement has no hypotheses, so the expected witness type is `True`. -/ theorem witness : True := trivial
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).