The Riemann hypothesis
Every non-trivial zero of the zeta function lies on the line Re(s) = 1/2.
▸Motivation
Riemann, 1859, in the only paper he wrote on number theory. A Clay Millennium Problem.
Its significance is that it is equivalent to the sharpest possible error term in the prime number theorem: the zeros control the fluctuation of the primes around their average density, and the real part of a zero is exactly the exponent in the error. Hundreds of results are published conditional on it.
Over ten trillion zeros have been checked and all lie on the line. That is worth almost nothing as evidence — the first counterexample to some analogous conjectures occurs beyond any computable range.
Bernhard Riemann, 1859. Clay Millennium Problem.
▸Lean API
import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
import Mathlib.NumberTheory.LSeries.RiemannZeta
namespace Conjectura.AN002
/-- Every non-trivial zero of the Riemann zeta function has real part `1/2`. The
trivial zeros are the negative even integers, excluded here by restricting to the
strip where the real part lies strictly between zero and one. -/
def goal : Prop :=
∀ s : ℂ, riemannZeta s = 0 → 0 < s.re → s.re < 1 → s.re = 1 / 2
end Conjectura.AN002▸Definition2
- riemannZetariemannZeta
def
- res.re
def
▸Related work1
- On the Number of Primes Less Than a Given MagnitudeBernhard Riemann · 1859
The original paper, where the hypothesis appears as an aside.
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem AN002 — The Riemann hypothesis
Every non-trivial zero of the zeta function lies on the line Re(s) = 1/2.
## Environment (fixed — do not assume anything newer)
- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`
If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.
## The exact statement I must prove
```lean
theorem solution : ∀ s : ℂ, riemannZeta s = 0 → 0 < s.re → s.re < 1 → s.re = 1 / 2 := by
sorry
```
## The file I submit
```lean
import Conjectura.Problems.AN002.Statement
namespace Submission
theorem solution : Conjectura.AN002.goal := by
sorry
end Submission
```
## The Lean definitions of every term in this problem
These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.
### riemannZeta
def
```lean
riemannZeta
```
Defined in Mathlib.
### re
def
```lean
s.re
```
Defined in Mathlib.
## Rules — submissions violating these are rejected automatically
1. **Do not change the name or type of `solution`.** It must satisfy the
statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
Declaring your own `goal`, or redefining a name it depends on, produces a
proof of a *different* statement and is rejected. This is the single most
common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
`Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
`snake_case` theorem names, `UpperCamelCase` types.
## What I want from you
Here is my argument in informal mathematics:
> [PASTE YOUR PROOF SKETCH HERE]
Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.Submissions are not open yet
Conjectura is in beta. You can read every statement, every definition and the Lean behind them, and download the exact files the checker uses — but proofs are not being accepted yet.
The reason is a deliberate order of operations. Accepting a proof means running a stranger’s code and standing behind a verdict, and no statement here yet carries a researcher’s name. A machine-checked answer to a question nobody has vouched for is worth very little, so the vouching comes first.
The English write-ups are also switched off during the beta. Nothing on this page is generated by a model.
Discussion
- Nothing yet.
Sign in to take part.