Number theory

Riemann Hypothesis

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.

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.Millennium.RiemannHypothesis
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "RiemannHypothesis.riemannHypothesis" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

RiemannHypothesis

Original conjecture source: FormalConjectures/Millennium/RiemannHypothesis.lean

Source type SHA-256: sha256:7024d428ede1c873b201a0801e42593ab9afd4e632c16c492678886797602547
Task id: fc-v2-riemannhypothesis-riemannhypothesis-3bedb9c82a8bc4e6bbbbb159-formalized
Task commitment: sha256:18511cda7d413194055236637866396d7cdd3aaddba8cadcaa6427e6f89a745c

References

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

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord