RiemannHypothesis.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 2 contain sorry, 0 declared as axioms

Riemann Hypothesis and its generalizations

The Riemann Hypothesis asserts that all non-trivial zeros of the Riemann zeta function $\zeta(s)$ have real part $\frac{1}{2}$. The trivial zeros are the negative even integers $-2, -4, -6, \ldots$. The hypothesis is one of the seven Millennium Prize Problems posed by the Clay Mathematics Institute.

The Generalized Riemann Hypothesis extends this to Dirichlet $L$-functions of primitive Dirichlet characters.

Note: the Extended Riemann Hypothesis (ERH) for Dedekind zeta functions is intentionally not stated here. Mathlib's NumberField.dedekindZeta is the naive Dirichlet series (LSeries), not a meromorphic continuation; outside the region of absolute convergence tsum returns junk 0, producing spurious zeros that make the naive foramlisation of the conjecture provably false. The ERH should be added once Mathlib provides a meromorphic continuation of the Dedekind zeta function.

References:

The Clay Institute
Wikipedia: Riemann hypothesis
Wikipedia: Generalized Riemann hypothesis
Wikipedia: Dedekind zeta function
J. Neukirch, Algebraic Number Theory, Springer (Grundlehren 322), 1999, Chapter VII, §5.
D. A. Marcus, Number Fields, Springer (GTM 81), 1977, Chapter VII.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean

theorem RiemannHypothesis.riemannHypothesis The Riemann Hypothesis sorry line 61 source
Source documentation
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.
L4DEL explanation
Every non-trivial zero of the Riemann zeta function has real part one half; the file marks this as open.
1. The statement is Mathlib's RiemannHypothesis proposition: for every complex s with zeta s = 0, s not of the form -2(n+1), and s not 1, the real part of s is 1/2.
2. The docstring describes it as the Clay Millennium Prize Problem; the attribute reads category research open and the proof body is sorry.
Sources and attribution: Pinned Lean source (1646ca16afd6)
depends on sorry what this means
Statement uses: RiemannHypothesis
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem riemannHypothesis : RiemannHypothesis := by
…
```
def GRH.trivialZeros Let $\chi$ be a Dirichlet character, trivialZeros is the set of trivial zeros of the Dirichlet $L$-function of $\chi$ which is always a set of non-positive integers line 74 source
Source documentation
Let $\chi$ be a Dirichlet character, trivialZeros is the set of trivial zeros of the Dirichlet $L$-function of $\chi$ which is always a set of non-positive integers.
- $\chi = 1$ then the Dirichlet $L$-function is the Riemann zeta function, having trivial zeroes at all negative even integers (exclude $0$).
- $\chi$ is odd, then the trivial zeroes are the negative odd integers.
- $\chi \neq 1$ is even, then the trivial zeroes are the non-positive even integers.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DirichletCharacter, Complex, Set, Int
Proof uses: ite, Eq, OfNat.ofNat, Set.ofPred, Exists, HMul.hMul, Neg.neg, HAdd.hAdd, DirichletCharacter.Odd, HSub.hSub
23 instances, coercions and auxiliary constants left out.
```
def trivialZeros {q : ℕ} (χ : DirichletCharacter ℂ q) : Set ℤ :=
…
```
theorem GRH.generalized_riemann_hypothesis The Generalized Riemann Hypothesis asserts that all the non-trivial zeros of the Dirichlet sorry line 83 source
Source documentation
The Generalized Riemann Hypothesis asserts that all the non-trivial zeros of the Dirichlet $L$-function $L(\chi, s)$ of a primitive Dirichlet character $\chi$ have real part $\frac{1}{2}$.

depends on sorry what this means
Statement uses: Nat, NeZero, DirichletCharacter, Complex, DirichletCharacter.IsPrimitive, Eq, DirichletCharacter.LFunction, OfNat.ofNat, Not, Membership.mem, Set, Set.image, Int, GRH.trivialZeros, Real, Complex.re, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem generalized_riemann_hypothesis (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
    (hχ : χ.IsPrimitive) (s : ℂ) (hs : χ.LFunction s = 0)
    (hs_nontrivial : s ∉ Int.cast '' trivialZeros χ) :
    s.re = 1 / 2 := by
…
```
Mentions: GRH.trivialZeros
theorem GRH.implies_riemannHypothesis GRH for $\chi = 1$ is RiemannHypothesis line 91 source
Source documentation
GRH for $\chi = 1$ is RiemannHypothesis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, DirichletCharacter.IsPrimitive, Complex, OfNat.ofNat, Nat, DirichletCharacter, ZMod, Eq, DirichletCharacter.LFunction, Not, Membership.mem, Set, Set.image, Int, GRH.trivialZeros, Real, Complex.re, HDiv.hDiv, RiemannHypothesis
Proof uses: Eq.mpr, riemannZeta, Neg.neg, HMul.hMul, HAdd.hAdd, Inv.inv, id, congr, congrArg, Eq.trans, True, implies_congr_ctx, forall_congr, congrFun', congrFun, DirichletCharacter.LFunction_modOne_eq, Exists, And, Set.ofPred, ite and 23 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem implies_riemannHypothesis :
    type_of% (generalized_riemann_hypothesis 1 1) ↔ RiemannHypothesis := by
…
```
Mentions: GRH.generalized_riemann_hypothesis