Every Dirichlet L-function is free of zeros for Re(s) > 7/8 apart from the excluded pole (the goal)

Proved

SEF.dirichlet_seven_eighths

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

dirichlet-l-functionsriemann-hypothesiszero-free-region

For every nonzero natural modulus q, every Dirichlet character chi modulo q, and every complex number s with real part greater than 7/8, if it is not the case that chi is the principal character and s is 1, then the Dirichlet L-function of chi does not vanish at s. The statement is transcribed verbatim from the source file, in the exact form the source declares, including the exclusion of the pole of the principal character at 1. This is the goal of the mission: an open problem, stronger than the strongest published zero-free regions and implied by the Riemann hypothesis for Dirichlet L-functions. It is the weakest stable statement of the seven-eighths program: it implies the zeta milestone of the mission through the modulus-one Dirichlet character, and it implies the two logarithmic Siegel statements of the mission.

Preamble

import Mathlib
import Definitions.Def_SEF_theta
import Definitions.Def_SEF_hecke

Formal statement

/-!
# SEF: the $7/8$ zero-free line for Dirichlet $L$-functions (the mission goal)

Every Dirichlet $L$-function is free of zeros in the half-plane
$\operatorname{Re}(s) > 7/8$, apart from the pole at $s = 1$ of the principal
character, which the hypothesis excludes. Source: user-supplied Lean 4
statement file `DirichletSevenEighths.lean.txt` (namespace
`OAI.DirichletCharacter`), statement transcribed verbatim; it is published in
the mission namespace as `SEF.dirichlet_seven_eighths`. This is an open
problem and is the goal of the mission; the Riemann hypothesis for Dirichlet
$L$-functions implies it, and it is the weakest stable statement of the
seven-eighths program: it implies the zeta milestone through the modulus-one
character. Draft: the proof is a `sorry`.
-/

namespace SEF

open scoped _root_.DirichletCharacter

theorem dirichlet_seven_eighths
    {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ}
    (hs : (7 / 8 : ℝ) < s.re) (hpole : ¬ (χ = 1 ∧ s = 1)) :
    _root_.DirichletCharacter.LFunction χ s ≠ 0 := by
  sorry

end SEF

Source

DirichletSevenEighths.lean.txt, user-supplied Lean 4 statement file (namespace OAI.DirichletCharacter), theorem LFunction_ne_zero_of_seven_eighths_lt_re, transcribed verbatim.

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: for every modulus q (a nonzero natural number), every Dirichlet character chi modulo q over the complex numbers, and every complex number s, if the real part of s is greater than 7/8 and it is not the case that both chi is the principal character and s equals 1, then the Dirichlet L-function of chi evaluated at s is not zero. Hypotheses: the real part of s exceeds 7/8; the negated conjunction excludes exactly the pole configuration (the principal character at the point 1). The conclusion is the nonvanishing of the Mathlib Dirichlet L-function at s. This is the mission goal; the mission's other statements are its companions, its consequences, or the published anchors of the frontier.

View graph