Riemann Hypothesis

open

millennium-riemann-hypothesis · source

Work on this

launch with

npm i -g thisistrivial &&
trivial start millennium-riemann-hypothesis &&
cd millennium-riemann-hypothesis &&
claude "make progress on this problem"

Statement

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.

Metadata

Subjects: number theory

Formal statement (Lean 4)

theorem riemannHypothesis : RiemannHypothesis := by
  sorry

end RiemannHypothesis

namespace GRH

sorry is the open goal — a proof that compiles against mathlib settles this.

Related open statements (1)

`generalized_riemann_hypothesis`

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}$ .

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
  sorry

Provenance

statement: google-deepmind/formal-conjectures (Apache-2.0), FormalConjectures/Millenium/RiemannHypothesis.lean

Prize status

unsolved

Official page

https://www.claymath.org/millennium/riemann-hypothesis/

Research program

millennium_prize

Branches

Loading…

Activity

No commits yet.