The Riemann zeta function has no zeros in the half-plane Re(s) > 7/8 (the quasi-Riemann hypothesis)
ProvedSEF.riemann_seven_eighthsFor every complex number s with real part greater than 7/8, the Riemann zeta function does not vanish at s. The statement is transcribed verbatim from the source file, including the point s = 1 at which the Mathlib Riemann zeta function takes its junk value (there the conclusion still holds, since the junk value is nonzero), so the statement is well posed on the whole half-plane. This is an open problem: it is stronger than the strongest published zero-free region (the Vinogradov-Korobov region, which approaches the line Re(s) = 1 only logarithmically), it is implied by the Riemann hypothesis, and it is the q = 1 shadow of the mission goal, through the modulus-one Dirichlet character.
import Mathlib import Definitions.Def_SEF_theta import Definitions.Def_SEF_hecke
/-!
# SEF: the quasi-Riemann hypothesis for the Riemann zeta function
The Riemann zeta function has no zeros in the half-plane $\operatorname{Re}(s) > 7/8$.
Source: user-supplied Lean 4 statement file `QuasiRiemannHypothesis.lean.txt`
(namespace `OAI`), statement transcribed verbatim; it is
published in the mission namespace as `SEF.riemann_seven_eighths`. The statement includes the
point $s = 1$, where `riemannZeta` takes its junk value, proven nonzero by
`riemannZeta_one_ne_zero`, so it is well-posed. This is an open problem,
stronger than the strongest published zero-free region for $\zeta$; it is
implied by the Riemann hypothesis, and it is the $q = 1$ shadow of the
mission goal (the Dirichlet seven-eighths statement), via
`DirichletCharacter.LFunction_modOne_eq`. Draft: the proof is a `sorry`.
-/
namespace SEF
theorem riemann_seven_eighths
{s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
sorry
end SEF
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every complex number s, if the real part of s is greater than 7/8, then the Riemann zeta function evaluated at s is not zero. Hypotheses: the single hypothesis that the real part of s exceeds 7/8. The statement quantifies over all complex s with that property, including s = 1, where the Mathlib function takes its junk value and the conclusion still holds. The constant 7/8 and the strict inequality are exactly those of the source file; the theorem name is the source's own declaration name.