AI Proved What?

AX02 (outside OpenAI’s math catalogue), October 2026

No zeros past 31/32, for every number field?

Cureton and Thorner, with AxiomProver, build on OpenAI’s quasi-Riemann hypothesis

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

Chapters

  1. 0:00The question
  2. 1:59The claim
  3. 4:33How the proof goes
  4. 6:48Where it stands

The claim, in plain words

This is AX02. In episode 003, OpenAI claimed that the Riemann zeta function has no zeros to the right of 7/8. Today: a paper that carries a weaker wall to every number field. A number field extends the rational numbers by a root of a polynomial. The Gaussian integers, a + bi, are the integers of one: the rationals with i adjoined. There, five splits as (2 + i)(2 − i), while three stays prime. Every number field K has a Dedekind zeta function: a sum over its ideals of one over the ideal’s norm to the power s, or a product over prime ideals. For the rational numbers, it is Riemann’s zeta. For the Gaussian integers, it is Riemann’s zeta times a Dirichlet L-function; our computer checks that at s = 2, both sides give 1.5067. Its zeros govern how prime ideals spread out.

Episode AX02 covers a preprint on the Hexagon server, A quasi-Riemann hypothesis for Dedekind zeta functions, by Dean Cureton and Jesse Thorner, listed as investigators. Theorem 1.1: if K is any number field, then its zeta function has no zeros with real part greater than 31/32; the point one, a pole, is excluded. Corollary 1.2: the same holds for the L-function of every finite-order Hecke character over K, wherever it is holomorphic. The abstract says these results were proved and formalized in Lean using AxiomProver. The repository’s README says the investigators directed the research and made the mathematical judgments, and that AxiomProver generated the proofs and the Lean formalization. The paper adds that the investigators take full responsibility for correctness. Version one, posted on October 12, claimed only 1 − 1/6000. Version two, on October 14, reaches 31/32.

So this is one AI lab’s result, built directly on another’s. The abstract opens with recent work on Artin’s primitive root conjecture, OpenAI’s preprint from episode 029, then says: following their strategy. The paper cites both of OpenAI’s zero-free preprints from episode 003, and says of the primitive root preprint: building on that paper, we prove the following result. It also warns that each use of OpenAI’s cyclotomic proofs must be justified again, for any field containing the twelfth roots of unity. The Lean builds on OpenAI’s too. The repository’s metadata lists adapted source from OpenAI’s math repository, for analytic number theory. In our count, 69 of its Lean files name that repository, two of them as reference only, and most of the paths they cite are in the folder of OpenAI’s own 7/8 Lean proof.

What it doesn’t claim

What is not claimed. Not the Riemann hypothesis: 31/32 is far from 1/2. Not a second proof of episode 003’s result: for the rational numbers, 31/32 is a weaker wall than 7/8, so it cannot confirm it. The paper says the refinement that reaches 7/8 is less suited to this work. Not a new primitive root theorem: it takes episode 029’s zero-free method, not its count of primes. And nothing is claimed on the boundary itself.

Where it stands

Preprint on Hexagon
Version 1, October 12, 2026 (claimed 1 − 1/6000); version 2, October 14, 2026 (31/32). Hexagon’s declarations: “A mix of human-written and AI-generated”; “Some parts of this contribution, but not all, have been checked and understood by a human.”
Independent expert review
None named in our sources. The paper thanks Ken Ono “for his helpful comments”.
Peer reviewed
No
Lean proof, by Axiom
AxiomMath/DedekindZetaZeroFree: README says only Lean’s three standard axioms; comparator configuration names both theorems; metadata review “agent-reviewed”, which it says “does not establish line-by-line correspondence between the informal and formal proofs”. Its README and metadata point to version 1, whose Theorem 1.1 states the older 1 − 1/6000; the formal statement has 31/32, as in version 2. Not built or run by us.

Last checked October 27, 2026. Where it stands. The paper is a Hexagon preprint. Its declaration says the text is a mix of human-written and AI-generated, and that some parts, but not all, have been checked and understood by a human. The paper thanks Ken Ono for helpful comments; no source we found names an independent expert review, and it is not peer reviewed. The repository was created on October 12. On the 13th, one commit changed its target from 5999/6000 to 31/32, and another added the Hecke corollary; GitHub’s build check passed on the final commit. The README says the proof uses only Lean’s three standard axioms, and a comparator configuration names the two theorems. The metadata calls the review agent-reviewed, and says this does not establish a line-by-line match with the paper. Our keyword scan of its 5,528 Lean files finds sorry only in the challenge statements, as intended. We did not build or run it.

What this changes in our record. Episode 003 still rests on OpenAI’s 7/8, with OpenAI’s own Lean; its wall for the rational numbers is weaker, so it is a follow-up, not a second check. Episode 029 still has no Lean proof from OpenAI, and its primitive root theorem is not formalized here. If it holds, no number field’s zeta function vanishes to the right of 31/32: OpenAI’s method, carried to every number field by Cureton and Thorner with AxiomProver, with a Lean proof we did not run, still waiting for an independent human referee. See our episodes 003 and 029.

How the proof goes

  1. History. History, as the paper tells it. In 1896, Hadamard and de la Vallée Poussin proved that zeta has no zeros with real part one or more, which gives the prime number theorem; Landau carried this to every Dedekind zeta function. A fixed wall theta, below one, with no zeros to its right, would give an error term of about x to the theta. The Riemann hypothesis says theta can be 1/2. The classical zero-free regions, of Vinogradov and Korobov, and for number fields of Sokolovskiĭ in 1968, hug the line real part one ever closer as the height grows. OpenAI’s preprints in episode 003 claimed fixed walls at 7/8 and 11/12, for zeta, and also Dirichlet L-functions and Hecke L-functions over ℚ(√−3); this paper calls that a monumental advance. And OpenAI’s primitive root preprint, our episode 029, claimed a wall at 1 − 10⁻⁶, for finite-order Hecke L-functions over cyclotomic fields that contain the twelfth roots of unity.
  2. The reciprocal. How the proof goes, in the paper’s account. First, fix a field F containing the twelfth roots of unity. Build a smoothed integral, f(Z), with one over the zeta function of F inside it. Its Mellin transform is exactly that reciprocal, times factors that never vanish. Now suppose f(Z) grows no faster than Z to the power 287/800, up to any small extra power. With a shift of 61/100 built into f, the transform continues to every s with real part above 61/100 plus 287/800, which is 31/32. So one over zeta has no pole there, and zeta has no zero. The saving is exactly 1/32; our computer checks the fractions.
  3. One average, two ways. The bound comes from estimating one weighted average in two ways, as in OpenAI’s primitive root paper. Cubic theta functions, from Kubota and Patterson, turn sextic twists into a family that a quadratic large sieve controls; that gives an upper bound. Poisson summation finds a main term proportional to f, and zero detection controls the other terms. The paper lists six ingredients, from ideal generators to zero detection, and checks each one for any such field. The hardest part, says the abstract, was formalizing Kazhdan and Patterson’s metaplectic forms, to cover every number field. New scales, a sharper zero detector and larger Euler domains, the paper says, improve the width from 1/6000 to 1/32.
  4. Descent. Last comes descent. Given any K, adjoin the twelfth roots of unity to get F. The extension is abelian, of degree at most four, and the zeta function of F is the zeta function of K times Hecke L-functions with no poles. So a zero for K would be a zero for F, which the main step forbids. For the rational numbers, F is the twelfth cyclotomic field, and its zeta function is Riemann’s zeta times three Dirichlet L-functions, of conductors 3, 4 and 12; our computer checks that factorization prime by prime. The Hecke corollary follows from a cyclic extension.

The numbers in the video

  • Ours: 61/100 + 287/800 = 31/32 and 39/100 − 287/800 = 1/32 (the paper’s equations 2.3–2.4); version 1’s 8/15 + 933/2000 = 1 − 1/6000.
  • Ours: the zeta function of the Gaussian integers at s = 2, as a lattice sum and as ζ(2) times Catalan’s constant: both 1.5067.
  • Ours: 78,438 prime ideals of ℤ[i] with norm up to 10⁶, against li(10⁶) − li(2) ≈ 78,627.
  • Ours: the first zeros of ζ(s)L(s, χ₋₄) on Re s = 1/2 are at heights 6.02 (the L-function) and 14.13 (ζ).
  • Ours: ζ of ℚ(ζ₁₂) is ζ(s) times the L-functions of the characters mod 12 of conductors 3, 4 and 12; the Euler factors agree for every prime 5 ≤ p < 5000.
  • Ours (keyword scan, not an audit): Axiom’s repository has 5,528 Lean files (1,658 vendored); sorry appears only in the two intended challenge statements; 69 files name openai/math, 2 of them as “Reference only; no source code copied”; 13 of the 15 OpenAI file paths they cite are in lean/OAI/NumberTheory/DirichletL, the folder of OpenAI’s 7/8 Lean proof.

Read the source

AI Proved What? is independent and not affiliated with Axiom Math or OpenAI.

Transcript

Read the full script

0:00The question

This is AX02. In episode 003, OpenAI claimed that the Riemann zeta function has no zeros to the right of 7/8. Today: a paper that carries a weaker wall to every number field. A number field extends the rational numbers by a root of a polynomial. The Gaussian integers, a + bi, are the integers of one: the rationals with i adjoined. There, five splits as (2 + i)(2 − i), while three stays prime. Every number field K has a Dedekind zeta function: a sum over its ideals of one over the ideal’s norm to the power s, or a product over prime ideals. For the rational numbers, it is Riemann’s zeta. For the Gaussian integers, it is Riemann’s zeta times a Dirichlet L-function; our computer checks that at s = 2, both sides give 1.5067. Its zeros govern how prime ideals spread out. History, as the paper tells it. In 1896, Hadamard and de la Vallée Poussin proved that zeta has no zeros with real part one or more, which gives the prime number theorem; Landau carried this to every Dedekind zeta function. A fixed wall theta, below one, with no zeros to its right, would give an error term of about x to the theta. The Riemann hypothesis says theta can be 1/2. The classical zero-free regions, of Vinogradov and Korobov, and for number fields of Sokolovskiĭ in 1968, hug the line real part one ever closer as the height grows. OpenAI’s preprints in episode 003 claimed fixed walls at 7/8 and 11/12, for zeta, and also Dirichlet L-functions and Hecke L-functions over ℚ(√−3); this paper calls that a monumental advance. And OpenAI’s primitive root preprint, our episode 029, claimed a wall at 1 − 10⁻⁶, for finite-order Hecke L-functions over cyclotomic fields that contain the twelfth roots of unity.

1:59The claim

Episode AX02 covers a preprint on the Hexagon server, A quasi-Riemann hypothesis for Dedekind zeta functions, by Dean Cureton and Jesse Thorner, listed as investigators. Theorem 1.1: if K is any number field, then its zeta function has no zeros with real part greater than 31/32; the point one, a pole, is excluded. Corollary 1.2: the same holds for the L-function of every finite-order Hecke character over K, wherever it is holomorphic. The abstract says these results were proved and formalized in Lean using AxiomProver. The repository’s README says the investigators directed the research and made the mathematical judgments, and that AxiomProver generated the proofs and the Lean formalization. The paper adds that the investigators take full responsibility for correctness. Version one, posted on October 12, claimed only 1 − 1/6000. Version two, on October 14, reaches 31/32. So this is one AI lab’s result, built directly on another’s. The abstract opens with recent work on Artin’s primitive root conjecture, OpenAI’s preprint from episode 029, then says: following their strategy. The paper cites both of OpenAI’s zero-free preprints from episode 003, and says of the primitive root preprint: building on that paper, we prove the following result. It also warns that each use of OpenAI’s cyclotomic proofs must be justified again, for any field containing the twelfth roots of unity. The Lean builds on OpenAI’s too. The repository’s metadata lists adapted source from OpenAI’s math repository, for analytic number theory. In our count, 69 of its Lean files name that repository, two of them as reference only, and most of the paths they cite are in the folder of OpenAI’s own 7/8 Lean proof. What is not claimed. Not the Riemann hypothesis: 31/32 is far from 1/2. Not a second proof of episode 003’s result: for the rational numbers, 31/32 is a weaker wall than 7/8, so it cannot confirm it. The paper says the refinement that reaches 7/8 is less suited to this work. Not a new primitive root theorem: it takes episode 029’s zero-free method, not its count of primes. And nothing is claimed on the boundary itself.

4:33How the proof goes

How the proof goes, in the paper’s account. First, fix a field F containing the twelfth roots of unity. Build a smoothed integral, f(Z), with one over the zeta function of F inside it. Its Mellin transform is exactly that reciprocal, times factors that never vanish. Now suppose f(Z) grows no faster than Z to the power 287/800, up to any small extra power. With a shift of 61/100 built into f, the transform continues to every s with real part above 61/100 plus 287/800, which is 31/32. So one over zeta has no pole there, and zeta has no zero. The saving is exactly 1/32; our computer checks the fractions. The bound comes from estimating one weighted average in two ways, as in OpenAI’s primitive root paper. Cubic theta functions, from Kubota and Patterson, turn sextic twists into a family that a quadratic large sieve controls; that gives an upper bound. Poisson summation finds a main term proportional to f, and zero detection controls the other terms. The paper lists six ingredients, from ideal generators to zero detection, and checks each one for any such field. The hardest part, says the abstract, was formalizing Kazhdan and Patterson’s metaplectic forms, to cover every number field. New scales, a sharper zero detector and larger Euler domains, the paper says, improve the width from 1/6000 to 1/32. Last comes descent. Given any K, adjoin the twelfth roots of unity to get F. The extension is abelian, of degree at most four, and the zeta function of F is the zeta function of K times Hecke L-functions with no poles. So a zero for K would be a zero for F, which the main step forbids. For the rational numbers, F is the twelfth cyclotomic field, and its zeta function is Riemann’s zeta times three Dirichlet L-functions, of conductors 3, 4 and 12; our computer checks that factorization prime by prime. The Hecke corollary follows from a cyclic extension.

6:48Where it stands

Where it stands. The paper is a Hexagon preprint. Its declaration says the text is a mix of human-written and AI-generated, and that some parts, but not all, have been checked and understood by a human. The paper thanks Ken Ono for helpful comments; no source we found names an independent expert review, and it is not peer reviewed. The repository was created on October 12. On the 13th, one commit changed its target from 5999/6000 to 31/32, and another added the Hecke corollary; GitHub’s build check passed on the final commit. The README says the proof uses only Lean’s three standard axioms, and a comparator configuration names the two theorems. The metadata calls the review agent-reviewed, and says this does not establish a line-by-line match with the paper. Our keyword scan of its 5,528 Lean files finds sorry only in the challenge statements, as intended. We did not build or run it. What this changes in our record. Episode 003 still rests on OpenAI’s 7/8, with OpenAI’s own Lean; its wall for the rational numbers is weaker, so it is a follow-up, not a second check. Episode 029 still has no Lean proof from OpenAI, and its primitive root theorem is not formalized here. If it holds, no number field’s zeta function vanishes to the right of 31/32: OpenAI’s method, carried to every number field by Cureton and Thorner with AxiomProver, with a Lean proof we did not run, still waiting for an independent human referee.

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.