∑math20

Number theory · Result 003

The quasi-Riemann hypothesis

3 papersLean

Proves that every Dirichlet L-function, including \(\zeta(s)\), is zero-free in \(\Re s\gt 7/8\), resolving the quasi-Riemann hypothesis. The same half-plane is zero-free for every finite-order Hecke L-function over \(\mathbb Q(\sqrt{-3})\). A companion gives a different proof of the zero-free half-plane \(\Re s\gt 11/12\).

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 3

First page of The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane $`\Re s\gt 7/8`$

The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane \(\Re s\gt 7/8\)

OpenAI · September 30, 2026

We prove that all finite-order Hecke L-functions over \(\mathbb Q(\sqrt{-3})\) and all Dirichlet L-functions are zero-free in the half-plane \(\Re s\gt 7/8\), with the principal pole at s = 1 allowed. In particular, the Riemann zeta function is zero-free in this half-plane, proving the quasi-Riemann hypothesis.

Read PDF Download Source

Cite
@misc{OAI:The-Quasi-Riemann-Hypothesis-September-30-2026,
  author = {{OpenAI}},
  title = {{The Quasi-Riemann Hypothesis:
            A Zero-Free Half-Plane $\mathrm{Re}(s)>7/8$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf}{OAI:The-Quasi-Riemann-Hypothesis-September-30-2026}},
  year = {2026}
}
First page of The Quasi-Riemann Hypothesis (alternate 11/12 proof)

The Quasi-Riemann Hypothesis (alternate 11/12 proof)

OpenAI · October 5, 2026

We establish the quasi-Riemann hypothesis by proving that every Dirichlet L-function, including Riemann's zeta function, has no zeros in the half-plane \(\mathop{\mathrm{Re}}\nolimits s\gt 11/12\). More generally, we prove the same zero-free half-plane for every finite-order Hecke L-function over \(K=\mathbb Q(\sqrt{-3})\). In particular, this rules out the existence of Landau–Siegel zeros.

Read PDF Download Source

Cite
@misc{OAI:The-Quasi-Riemann-Hypothesis-October-5-2026,
  author = {{OpenAI}},
  title = {{The Quasi-Riemann Hypothesis}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026/paper2.pdf}{OAI:The-Quasi-Riemann-Hypothesis-October-5-2026}},
  year = {2026}
}
First page of Uniform exclusion of Landau–Siegel zeros

Uniform exclusion of Landau–Siegel zeros

OpenAI · October 1, 2026

We prove the uniform exclusion of Landau–Siegel zeros. There is an absolute constant c > 0 such that every real zero \(\beta\in(0,1)\) of every primitive nonprincipal real Dirichlet L-function of conductor q ≥ 3 satisfies \((1-\beta)\log q\ge c\).

Read PDF Download Source

Cite
@misc{OAI:Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026,
  author = {{OpenAI}},
  title = {{Uniform exclusion of Landau--Siegel zeros}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026/paper.pdf}{OAI:Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The quasi-Riemann hypothesis asks for a fixed zero-free half-plane \(\Re s>\theta\) with \(\theta<1\). The formalization gives \(\theta=7/8\) for the Riemann zeta function and every Dirichlet \(L\)-function, uniformly over all positive moduli and all characters. It also establishes the same bound for finite-order Hecke \(L\)-functions over \(\mathbb Q(\sqrt{-3})\).

The principal-character poles at \(s=1\) are excluded in the Dirichlet and Hecke statements. The paper's later applications are not included.

The formalized result gives a uniform logarithmic exclusion region for Landau–Siegel zeros. There is one constant \(c>0\) such that every primitive nonprincipal real Dirichlet character of conductor \(q\ge3\) and every real zero \(0<\beta<1\) of its \(L\)-function satisfy \(1-\beta\ge c/\log q\).

Both character parities are included. No explicit value of \(c\) is given. This excludes real zeros in \(1-c/\log q<\beta<1\), but does not rule out real zeros elsewhere in \((0,1)\).

Comparator links

ResultComparator statement
Riemann zeta \(7/8\) boundQuasiRiemannHypothesis.lean
Dirichlet \(L\)-function \(7/8\) boundDirichletSevenEighths.lean
Finite-order Hecke \(L\)-function \(7/8\) boundHeckeSevenEighths.lean
Uniform real-zero gapSiegelZeros.lean

Scope note on GitHub →