feat(Millennium): Add Riemann Hypothesis (from Mathlib)

FormalConjectures/Millenium/GeneralizedRiemannHypothesis.lean → FormalConjectures/Millenium/RiemannHypothesis.lean

@@ -1,5 +1,5 @@
 /-
-Copyright 2025 The Formal Conjectures Authors.
+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.
@@ -17,11 +17,39 @@ limitations under the License.
 import FormalConjectures.Util.ProblemImports
 
 /-!
-# Generalized Riemann Hypothesis
+# Riemann Hypothesis and Generalized Riemann Hypothesis
 
-*Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Generalized_Riemann_hypothesis)
+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.
+
+*References:*
+- [The Clay Institute](https://www.claymath.org/wp-content/uploads/2022/05/riemann.pdf)
+- [Wikipedia: Riemann hypothesis](https://en.wikipedia.org/wiki/Riemann_hypothesis)
+- [Wikipedia: Generalized Riemann hypothesis](https://en.wikipedia.org/wiki/Generalized_Riemann_hypothesis)
 -/
 
+section RiemannHypothesis
+
+/-- 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](https://www.claymath.org/wp-content/uploads/2022/05/riemann.pdf).
+
+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`. -/
+@[category research open, AMS 11]
+theorem riemannHypothesis : RiemannHypothesis := by
+  sorry
+
+end RiemannHypothesis
+
 namespace GRH
 
 /-- Let $\chi$ be a Dirichlet character, `trivialZeros` is the set of trivial zeros of the

FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean

@@ -15,7 +15,7 @@ limitations under the License.
 -/
 
 import FormalConjectures.Util.ProblemImports
-import FormalConjectures.Millenium.GeneralizedRiemannHypothesis
+import FormalConjectures.Millenium.RiemannHypothesis
 
 /-!
 # Artin's conjecture on primitive roots