Claimed Collaborative

Quasi-Riemann hypothesis: no zeros of zeta or any Dirichlet L-function with real part above 7/8

A Lean-formalized proof that neither the Riemann zeta function nor any Dirichlet L-function has a zero with real part greater than 7/8, the first fixed zero-free half-plane short of the line where real part equals 1, which also rules out Landau-Siegel zeros but leaves the Riemann hypothesis itself open.

Lab: OpenAI
Model: Unreleased internal OpenAI model, not named in the release
Field: Mathematics
Date: 2026-10-06
Problem posed: 1859 · open 167 yrs

Sources

What was found

The main theorem states that every finite-order Hecke L-function over $\mathbb{Q}(\sqrt{-3})$ and every Dirichlet L-function, including $\zeta(s)$ , is zero-free in $\Re s > 7/8$ , the principal pole at $s=1$ excepted. The quasi-Riemann hypothesis asks for any fixed $\sigma_0 < 1$ with no zeros to the right of it; the classical zero-free regions of de la Vallée Poussin and Vinogradov-Korobov shrink toward $\Re s = 1$ with height, and zero-density estimates such as Guth and Maynard's bound how many zeros there are rather than excluding them. A fixed half-plane gives the prime number theorem with error $O(x^{7/8+\varepsilon})$ . The paper works through Kubota's metaplectic theory and Patterson's cubic theta series, with sextic large-sieve estimates extending Goldmakher, Louvel and Blomer, using Dunn and Radziwiłł's unconditional cusp expansions. A companion manuscript reaches the weaker half-plane $\Re s > 11/12$ by a different proof, and a third proves $(1-\beta)\log q \ge c$ for every real zero $\beta$ of every primitive real character of conductor $q \ge 3$ . The Lean statement for zeta is a single line against Mathlib's own definition, OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re, with separate Comparator challenges for the Dirichlet and Hecke versions and for the Siegel-zero bound, each permitting only propext, Quot.sound and Classical.choice.

Novelty check

Read the three manuscripts' introductions and the Lean scope note lean/docs/003.md at commit adc7f1241b42e322a6451854ab7e4b4c146bf78a on 2026-10-07. The paper takes the name quasi-Riemann hypothesis from Billington, Cheng, Schettler and Suriajaya (2025) and the uniform formulation over Dirichlet characters from Friedlander and Goldston (1997), and cites no earlier proof of any fixed half-plane; none was found in a web search, and no such half-plane is known unconditionally in the standard literature. For Landau-Siegel zeros the unconditional state of the art before this was Siegel's ineffective 1935 bound; Yitang Zhang's 2022 preprint claims a weaker bound of polylogarithmic strength. No prior registry entry covers either statement; 2026-08-10-zeta-zeros-critical-line concerns the proportion of zeros on the critical line, a different question.

Caveats and known objections

Graded claimed despite a Lean development, for the reason the Navier-Stokes entry set: the catalogue records its review status as unchecked and nobody outside OpenAI is on record as having run the Comparator challenge or read the argument. What would move it is narrow here, because the zeta statement is anchored on Mathlib's own riemannZeta, so a successful independent Comparator run would support formal on its own. The formalization is very large, about 2,900 Lean files and 487,000 lines under the Dirichlet L-function directory and about 70,000 more for the Siegel-zero bound; a text search found no sorry or axiom declarations, which is not a build. The Siegel-zero manuscript gives no explicit constant, though the half-plane alone already implies $1-\beta \ge 1/8$ for every real zero, so its interest lies in the independent route rather than the bound. Autonomy is graded collaborative, the weakest reading consistent with OpenAI's account that the model produced the result: the README names the zero-free-region work as an exception to the fixed single-agent procedure without saying what was done differently, and says the $11/12$ write-up was edited by humans. Nothing here bears on the Riemann hypothesis, which places the zeros on $\Re s = 1/2$ ; press summaries describing this as progress toward it overstate the connection.

Nobody outside the lab has checked this yet.

Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.

Submit a check Challenge the grade

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-07AddedEntered the registry graded Claimed and Collaborative.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Community discussion

Hacker NewsSharing AI progress in mathematics↗Hacker NewsThe Quasi-Riemann Hypothesis [pdf]↗

Graded claimed for verification and collaborative for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Quasi-Riemann hypothesis: no zeros of zeta or any Dirichlet L-function with real part above 7/8. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-06-quasi-riemann-hypothesis

BibTeX

@misc{whataifound-openai-2026-hypothesis,
  title        = {Quasi-Riemann hypothesis: no zeros of zeta or any Dirichlet L-function with real part above 7/8},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by OpenAI. Verification: Claimed. Autonomy: Collaborative.},
  url          = {https://whataifound.org/finding/2026-10-06-quasi-riemann-hypothesis}
}

Related findings

Claimed722 manuscripts in 372 result families from an unreleased OpenAI modelOpenAI · 2026-10-06 ClaimedHuang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputsAxiom Math · 2026-09-17 ClaimedBounded prime gaps improved to 212, with a Lean certificate of the deductionAxiom Math · 2026-09-03

number-theory riemann-zeta l-functions lean formalization argument

← All mathematics findings in the registry