AI Proved What?

Episode 003, October 2026

A wall at 7/8

The quasi-Riemann hypothesis: no zeros past real part 7/8

Covers result 003 in OpenAI’s catalog: all 3 papers. See its connections to other results and the work it cites.

Play Episode 003: No zeros past 7/8? The critical strip, its first zeros on the line at one half, and a gold wall at real part seven eighths.

8:44. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The claim: a wall for the zeros
  2. 0:38Counting primes
  3. 1:25The zeta function and its zeros
  4. 2:19Zeros make the waves
  5. 3:08What was known
  6. 4:04The theorem
  7. 5:12How the proof goes
  8. 7:08The Lean proof
  9. 8:05Why it matters, and the caveats

The claim, in plain words

The Riemann zeta function, ζ(s) = 1 + 1/2s + 1/3s + ⋯, is also a product over the primes, so its zeros control how regularly the primes are spread out. Apart from easy zeros at −2, −4, −6, …, every zero lies in the strip where the real part of s is between 0 and 1. A zero with real part β adds a wave of size about xβ to the error when you count primes up to x. The Riemann hypothesis says every zero in the strip has real part ½.

The quasi-Riemann hypothesis asks for much less: some fixed wall θ < 1 with no zeros to its right, at any height. Until now every proven zero-free region got thinner and thinner as the height grew, so no fixed wall was known.

Result 003 claims the wall θ = 7/8: no zeros with real part greater than 7/8, for ζ(s) and, with the same wall, for every Dirichlet L-function, and also for every finite-order Hecke L-function over ℚ(√−3), the Eisenstein integers. For ζ, the zeros in the strip come in mirror pairs around the line at ½, so they would all lie in the band from 1/8 to 7/8.

What would follow

  • The prime number theorem with a power-saving error, π(x) = li(x) + O(x7/8 log x), by a standard argument. The best error previously proved saved less than any power of x.
  • No Siegel zeros: every real zero of every real Dirichlet L-function has real part at most 7/8. A short companion paper proves a weaker form of this by a different method.
  • The main paper also claims Vinogradov’s conjecture on the least quadratic non-residue, with a bound polynomial in log p. That claim, like the prime number theorem bound, is not part of the Lean proof.

What it doesn’t claim

It is not the Riemann hypothesis. It says nothing about zeros with real part between 1/8 and 7/8, and the paper says so itself: “The Riemann hypothesis remains open.” The wall is not claimed for L-functions of other number fields, or for L-functions of elliptic curves. On its own, a wall at 7/8 does not improve the best known results on primes in short intervals or on the least prime in an arithmetic progression.

Where it stands

Posted as a preprint
OpenAI, main paper dated September 30, 2026
Peer reviewed
Not yet
Checked in Lean
OpenAI published a Lean proof of the main theorem (scope notes)

Last checked October 19, 2026. The claim has not been withdrawn. OpenAI’s Lean formalization covers the 7/8 statements for ζ(s), for every Dirichlet L-function and for the Hecke family over ℚ(√−3), plus the Siegel-zero bound. It does not cover the paper’s later applications or the alternate 11/12 proof. We have not run the Comparator check ourselves, and OpenAI’s Lean catalog lists its formalizations as written by an AI agent, with review status “unchecked.” OpenAI’s README says work on this zero-free region was an exception to its fixed procedure, and that the 11/12 write-up was human edited for readability.

How the proof goes

  1. Go to the Eisenstein integers. Counting the numbers a + bω of each norm gives the zeta function of ℚ(√−3), which factors as ζ(s) · L(s, χ−3). In the same way every Dirichlet L-function is a factor of a Hecke L-function over ℚ(√−3), so a zero past 7/8 anywhere would be a zero of one of those. There the arithmetic has sixth roots of unity, sextic residue symbols, and Kubota’s cubic theta function, whose symmetry the proof exploits.
  2. The alternate proof, to 11/12. It is enough to show that a Möbius sum A(D) of length D is at most about D11/12. The proof hides it in a crowd of sums twisted by sextic residue symbols and shows, using the cubic theta function, Poisson summation and a large sieve, that the twisted sums are only about √D on average. When the twisting label is a sixth power of a prime, the twist does almost nothing, so about D1/6 rows are near-copies of the target. If the target were larger than D11/12, those copies alone would exceed the average.
  3. The main proof, to 7/8. A probe built from cubic Gauss sums secretly contains 1/L. If the rightmost zero of the whole family had real part β, the probe would have to reach size about Zβ − 11/16, while moment and large-sieve bounds cap it at about Z3/16. Both hold only if β ≤ 11/16 + 3/16 = 7/8. Each step creates new twisted L-functions, so the argument runs over the whole family of Hecke L-functions at once. Most of the 199 pages control those other terms.

The Lean statement

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0

This is the challenge statement that OpenAI’s setup checks with the Comparator tool. A passing check guarantees that the proof proves exactly this statement, about Mathlib’s riemannZeta, using only Lean’s standard axioms (propext, Quot.sound, Classical.choice). Beyond Mathlib and other libraries, the proof uses 2,924 of OpenAI’s own Lean files, about 486,000 lines. A search of those files found no sorry and no new axioms, but a search is not a substitute for running the check.

The numbers in the video

  • The first zeros of ζ(s) have heights 14.1347…, 21.0220…, 25.0109… (computed with mpmath). Platt and Trudgian (2021) verified the Riemann hypothesis up to height 3·1012, about 1.24·1013 zeros.
  • For every x from 3 to 108, π(x) − li(x) stays between −√x and √x; the largest ratio is about 0.78, just below x = 11 (sieve and mpmath). At x = 108 the difference is −754.4.
  • The explicit-formula plot rebuilds ψ(x) from 1 to 100 pairs of zeros. The waves at real part 0.95 are hypothetical, for comparison.
  • Zero-free region widths use the explicit constant 5.558691 of Mossinghoff, Trudgian and Yang: about 0.0039 at height 1020; at 10100 the best known regions are about a thousandth wide. The video draws them five times wider.
  • Primes below 100,000 ending in 1, 3, 7 and 9: 2,387, 2,402, 2,411 and 2,390.
  • The crowd of bars in the proof sketch is a cartoon of the mean-square argument, not data.

Read the source

The 3 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The claim: a wall for the zeros

Result 003 in OpenAI’s math repository claims something number theorists have wanted for more than a century: a fixed wall that the zeros of the Riemann zeta function can never cross. This is not the Riemann hypothesis. That famous conjecture says every one of these zeros sits on a single line. The new claim is weaker: no zero lies to the right of 7/8. But until now, nobody had proved a wall like this at any distance at all. And for the first time in this series, the main theorem comes with a proof a computer can check. To see why it matters, start with the primes.

0:38Counting primes

Count the primes up to x, and call the count π(x). Up close it’s an irregular staircase. From far away it hugs a smooth curve, guessed by Gauss as a teenager: the logarithmic integral of x. In 1896, Hadamard and de la Vallée Poussin proved that their ratio tends to one: the prime number theorem. The deeper question is the size of the error, the gap between the staircase and the curve. In the data, the error is small. All the way to a hundred million, it stays below the square root of x. But what can anyone prove? The best proven bound is only a little smaller than x itself. No one could show the error is below x to the 0.99, or below x to any power less than one.

1:25The zeta function and its zeros

The key is a function Riemann studied in 1859: zeta of s, the sum of one over n to the s. Euler had noticed that it’s also a product over the primes. So every fact about the primes is hiding inside zeta. Riemann let s be a complex number. Zeta then extends to the whole plane, except for a single pole at s equals one. And it has zeros. Apart from easy ones at the negative even numbers, every zero lies in a vertical strip, between real part zero and real part one. The first few sit at heights 14.13, 21.02, and 25.01, all on the line with real part 1/2. The Riemann hypothesis says every zero in the strip is on that line. Computers have checked more than twelve trillion of them. Nobody can prove it.

2:19Zeros make the waves

Why do the zeros matter so much? The explicit formula, from Riemann and von Mangoldt, rebuilds the prime staircase from the smooth curve plus one wave for each zero. A zero with real part beta makes a wave whose size grows like x to the beta. Zeros on the half line make waves the size of the square root of x. That’s the size of the error we see. But a single zero farther right, say at real part 0.95, would make a wave that eventually swamps all the others. So the rightmost zero sets the size of the error. Prove there are no zeros to the right of some wall, at theta less than one, and the error is at most about x to the theta. A wall like that, at any distance short of one, is what people call the quasi-Riemann hypothesis.

3:08What was known

What was known? The 1896 proof showed there are no zeros on the line with real part one. A few years later, de la Vallée Poussin pushed a little further, to a thin zero-free region just left of that line. But the region gets thinner as you climb. At height ten to the twenty, far above where every zero has been checked, it’s only about four thousandths wide. At height ten to the hundred, about a thousandth. Vinogradov and Korobov slowed the shrinking in 1958, but it still shrinks to nothing. For more than a century, no one could prove a wall of fixed width. The same problem haunts zeta’s cousins, the Dirichlet L-functions, which count primes in arithmetic progressions, like primes ending in seven. They carry an extra worry: a single real zero, sneaking extremely close to one. It’s called a Siegel zero, and no one could rule it out.

4:04The theorem

Here is what result 003 claims. Every Dirichlet L-function, including zeta itself, has no zeros with real part greater than 7/8. One fixed wall, at every height, for every one of them. For zeta, the zeros in the strip come in mirror pairs around the half line, so they’re trapped in a band from 1/8 to 7/8. And the same wall holds for a family of L-functions built from the Eisenstein integers, which is where the proof does its work. If it’s right, the consequences are big. The prime number theorem gets its first error bound with a power saving: x to the 7/8, up to logarithms. Siegel zeros are ruled out completely. The paper also claims to prove a long-standing conjecture of Vinogradov about the smallest non-square modulo a prime. Neither that nor the prime counting bound is part of the computer-checked proof. What it doesn’t do: it says nothing about zeros between 1/8 and 7/8. The Riemann hypothesis, which would put them all on the half line, is still open. The paper says so itself.

5:12How the proof goes

How could anyone build such a wall? The proof takes a detour through the Eisenstein integers: numbers a plus b omega, where omega is a complex cube root of one. They form this hexagonal lattice. Count the lattice points of each size, and you get a new zeta function. It splits exactly into zeta times one Dirichlet L-function. So a zero of zeta would also be a zero in the Eisenstein world. And that world has extra symmetry: cube roots and sixth roots of one, and a cubic cousin of the classical theta function. Here’s the idea of the shorter, alternate proof, which reaches 11/12. To rule out zeros past a wall, it’s enough to show that a sum of Möbius values, each plus one, minus one or zero, stays small. Call that sum the target. Now hide the target in a crowd. Twist it by a sixth power residue symbol, one twist for each label u, roughly D of them. A hard theorem, built on that cubic theta function and a large sieve, shows the twisted sums are small on average: about the square root of D, the size of random noise. Here’s the trick. When the label is a perfect sixth power, the twist does almost nothing. That row is nearly a copy of the target, and there are about D to the one sixth such copies. If the target were bigger than D to the 11/12, the copies alone would blow the budget. So the target is small, and there are no zeros past 11/12. The main paper, 199 pages, builds a sharper machine. A zero at real part beta would make a carefully built probe as large as Z to the beta minus 11/16. Other bounds cap the probe at Z to the 3/16. Both can hold only if beta is at most 11/16 plus 3/16: 7/8. And every step spawns new twisted L-functions, so the argument must work for the whole family at once.

7:08The Lean proof

Unlike our first two episodes, this claim comes with a proof in Lean, a language for computer-checked mathematics. Here is the statement: for every complex number s with real part greater than 7/8, zeta of s is not zero. Behind it sit about 2,900 files, nearly half a million lines, written by an AI agent. OpenAI set it up for a checking tool called Comparator. A passing check guarantees that the proof proves exactly this statement, using the zeta function from Lean’s math library and only Lean’s usual axioms. OpenAI also formalized the Dirichlet and Eisenstein versions, and the Siegel zero bound. We haven’t run the check ourselves. And OpenAI’s catalog lists its Lean work as written by an AI agent, with review status unchecked. A Lean proof checks that one statement, not the paper’s text, and not the extra claims, like Vinogradov’s conjecture.

8:05Why it matters, and the caveats

If it holds, this is one of the biggest advances in analytic number theory in decades: the first fixed wall for the zeros, and the end of the Siegel zero problem, in one stroke. The caveats. This is a preprint, and it hasn’t been peer reviewed. OpenAI says work on this zero-free region was an exception to its fixed procedure, and that people edited the 11/12 write-up for readability. The computer proof covers the main theorem, but we haven’t run the check ourselves. And the Riemann hypothesis is untouched. A wall at 7/8. Not yet the line at 1/2.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.