Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

No zeros of ζ\zetaζ with 12<Re⁡s<1\tfrac12<\operatorname{Re} s<121​<Res<1 above height 222

Open
zeta_ne_zero_of_strip_of_two_lt_abs_im

by Gabewhigham · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryconjecturemillennium-prizenumber-theoryzeta-functions

Let ζ\zetaζ denote the Riemann zeta function. The assertion is that ζ\zetaζ has no zero strictly to the right of the critical line inside the critical strip, at height larger than 222:

12<Re⁡s<1  and  ∣Im⁡s∣>2 ⟹ ζ(s)≠0.\tfrac12<\operatorname{Re} s<1 \ \text{ and } \ |\operatorname{Im} s|>2 \ \Longrightarrow\ \zeta(s)\neq 0.21​<Res<1  and  ∣Ims∣>2 ⟹ ζ(s)=0.

This is open: it is the Riemann hypothesis with the two parts that are unconditionally known removed. Indeed, non-vanishing for Re⁡s≥1\operatorname{Re} s\ge 1Res≥1 is classical (Mathlib's riemannZeta_ne_zero_of_one_le_re), and non-vanishing in the low-lying rectangle 0<Re⁡s<10<\operatorname{Re} s<10<Res<1, ∣Im⁡s∣≤2|\operatorname{Im} s|\le 2∣Ims∣≤2 is an explicit estimate on the completed zeta function. Together with those two facts, the statement above is equivalent to the half-plane form of the Riemann hypothesis, Re⁡s>12⇒ζ(s)≠0\operatorname{Re} s>\tfrac12\Rightarrow\zeta(s)\neq 0Res>21​⇒ζ(s)=0, and hence to the Riemann hypothesis itself.

Phrasing the remaining open problem this way isolates exactly the region where the difficulty lies: a bounded-real-part, unbounded-height region on one side of the critical line. Any progress of zero-density or zero-free-region type applies to it directly.

Formalization note. riemannZeta is Mathlib's zeta function; |s.im| is the absolute value of the imaginary part of sss.

Preamble
import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.LSeries.Nonvanishing

open Complex
Formal statement
theorem zeta_ne_zero_of_strip_of_two_lt_abs_im (s : ℂ) (h0 : 1 / 2 < s.re) (h1 : s.re < 1)
    (him : 2 < |s.im|) : riemannZeta s ≠ 0 := by sorry
Source
https://en.wikipedia.org/wiki/Riemann_hypothesis

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me