---
type: analysis
slug: research-openai-s-siegel-zero-proof-holds-up-in-three-expert-rewrites-and-lean-checks
title: "OpenAI's Siegel-zero proof holds up in three expert rewrites and Lean checks, but none are refereed"
description: "At least three mathematicians, plus Ben Green's note, have independently rewritten, simplified or made explicit OpenAI's nine-page argument, and none reports a gap. A Lean check passed on two independent kernels. Formal peer review has not started, and the formal statement is narrower than the headline."
published_at: 2026-11-08T16:00:00.000Z
topics: ["openai","research"]
source_urls: ["https://terrytao.wordpress.com/2026/10/19/a-sketch-of-the-proof-of-non-existence-of-siegel-zeroes","https://arxiv.org/abs/2610.15483","https://mathworld.wolfram.com/Landau-SiegelZero.html","https://arxiv.org/abs/2610.21099","https://arxiv.org/html/2610.30476","https://github.com/jmreilly1113/siegel-zeros-audit","https://github.com/openai/math","https://github.com/openai/math/tree/main/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026","https://www.scientificamerican.com/article/the-most-exciting-claims-from-openais-heap-of-new-proofs/"]
author: "Andrey Reshetnikov"
author_profile: https://newruntime.com/owner-profile.md
---
Siegel zeros (Landau–Siegel zeros) are hypothetical real zeros of Dirichlet L-functions lying very close to s = 1. Whether they exist has been open for about a century. Their possible existence is why many results on how primes are distributed across arithmetic progressions carry constants that cannot be computed. In early October 2026, OpenAI published 719 machine-generated manuscripts in its public openai/math repository. One was a nine-page paper credited only to "OpenAI": "Uniform exclusion of Landau–Siegel zeros," dated October 1. It claims there is an absolute constant c > 0 with (1−β)log q ≥ c for every real zero β of L(s,χ). Two companion "quasi-Riemann hypothesis" papers claim zero-free regions out to real part 7/8 and 11/12.

On October 19, Terence Tao posted a sketch of Ben Green's reformulation of the proof. Our newsroom flagged the story because the result is exceptional and Tao says some of the related arguments are "still being digested." For AI builders this is a test case: an AI-generated proof of a famous open problem is now being checked by humans and by formal tools in public, and the details of that checking matter more than the headline.

## What we checked

- **Have independent number theorists checked the complete proof and identified any unresolved assumptions or gaps?** partly confirmed. Several mathematicians have independently reconstructed the full argument: Banks gives a detailed proof with explicit constants, Kerr a simpler pigeonhole-plus-Masser proof, Guo an explicit elementary proof, and Ben Green a reformulation that Tao sketches. None of them reports a gap. None of this work has been refereed, though. Banks's reliance on a cited computation for small conductors was not checked independently, and Tao's sketch itself 'cheats' on a few cases. [2][4][5][1][3]
- **Has the Siegel-zero result been machine-verified in Lean, and what does that verification cover?** partly confirmed. An independent audit reran OpenAI's Lean formalization of this result family on the Lean FRO comparator plus a second, independently written kernel (nanoda), using only standard axioms. Both accepted it. The audit also formalized the paper's own Lemma 3. Its author says plainly that the audit 'is not a proof of the theorem' and has not been refereed. Whether the formal statement matches the paper still needs a human audit. [6][7]

## What we found

- Tao's post sketches Green's version of the argument: an injectivity lemma via resultants, an Archimedean bound via Hadamard's inequality, and a non-Archimedean bound. Together they give a nontrivial upper bound on primes at which D is a quadratic non-residue. Tao says he makes 'minor assumptions and cheats': he takes D negative, excludes D = −1, and assumes an auxiliary polynomial is irreducible. Green's note handles the general case. In the comments, Green says a 'communal writeup' aimed at traditional publication is coming. [1]
- William Banks (arXiv:2610.15483, submitted October 11) gives a detailed direct proof of the OpenAI argument with explicit constants: δ₀ = 3.0×10⁻³ for q ≥ 10¹⁰. Combined with a computation by Lu, Zaman and Zhao, this extends to all q ≥ 3. MathWorld reports that Banks checked the argument line by line but did not verify the small-conductor computation himself, and that he asks for further independent scrutiny. [2][3]
- Bryce Kerr (arXiv:2610.21099, October 15) simplifies the proof. He replaces the interpolation-determinant analysis with the pigeonhole principle and a theorem of Masser. Victor Zhenyu Guo (arXiv:2610.30476, October 21) gives an elementary proof with the explicit constant c = 1/100 for all conductors q ≥ 3, and discloses ChatGPT assistance. Independent routes reaching the same conclusion are meaningful evidence, but they are still preprints. [4][5]
- The comments on Tao's post act as informal expert review. Felipe Voloch, a specialist in Stepanov's method, calls the proof 'very nice' and says he is 'baffled' by it. Will Sawin traces the key injectivity fact back to Sylvester (1852). Commenters caught small typos, which Tao corrected. No one in the comments reported a substantive gap. Green also notes that ChatGPT failed to find the correct Sylvester reference. [1]
- An independent audit by Joseph Reilly reran OpenAI's Lean formalization on the Lean FRO comparator and on a second kernel (nanoda), with network access blocked and only standard axioms. Both accepted it. The audit also formalized the paper's own Lemma 3 and ran small-N numerical checks. Reilly writes that the audit 'is not a proof of the theorem' and that none of the related works 'has been refereed.' [6]
- OpenAI's repository says results are 'at different verification stages,' that about 42% of top-line results are formalized, and that some unformalized results may contain issues. The Siegel-zero paper's directory names no human authors. Scientific American reported on October 8 that nobody, including OpenAI, had read all the material, and that some proofs in the release had been retracted after outside scrutiny. It also quotes Hector Pasten saying the Siegel-zero result 'settles the question.' [7][8][9]

## What it means

The evidence is strong but has not been through the formal process. Several mathematicians have reconstructed the short Siegel-zero argument by different routes, at least one with explicit constants, and nobody has reported a gap. Two Lean kernels accept a formalization. That is more scrutiny than most new results get within three weeks. Still, nothing has been refereed. MathWorld notes that the result excludes real zeros only in a window near 1 (1 − c/log q < β < 1); it does not rule out every real zero. The harder 199-page quasi-Riemann papers are, in Tao's words, still being digested. Builders and writers should describe this as "a claim that independent experts have widely reproduced," not as "proven," and should keep the nine-page Siegel result separate from the much longer and less-checked QRH claims.

For people building AI-for-math pipelines, the lesson is about verification method. Confidence here came from three things: independent human re-derivations, a second-kernel replay of the Lean proof, and expert commentary in public. Benchmark scores played no part. Lean acceptance establishes the formal statement. It does not establish that the formal statement means what the paper claims, and the audit's author says exactly that. The release also shows a known weakness: models are unreliable at citations (ChatGPT could not find the Sylvester reference). Mass releases of uneven quality also cost expert reviewers time and attention. Ship formal artifacts with independent kernel replays, and ship human-readable proofs short enough for experts to check.

## Still open

- Will the communal writeup Green announced pass journal refereeing, and when?
- Does the Lean main-theorem statement exactly match the paper's claim? Has anyone formally audited the statement itself, beyond kernel acceptance?
- Have the 7/8 and 11/12 quasi-Riemann papers received comparable independent checking?
- Which human collaborators, if any, edited the OpenAI Siegel-zero manuscript, and how much did they contribute?

## Sources

1. [Terence Tao: A sketch of the proof of non-existence of Siegel zeroes](https://terrytao.wordpress.com/2026/10/19/a-sketch-of-the-proof-of-non-existence-of-siegel-zeroes)
2. [Banks: On the OpenAI proof that Landau–Siegel zeros do not exist](https://arxiv.org/abs/2610.15483)
3. [MathWorld: Landau-Siegel Zero](https://mathworld.wolfram.com/Landau-SiegelZero.html)
4. [Kerr: A simpler proof that there are no Landau–Siegel zeros](https://arxiv.org/abs/2610.21099)
5. [Guo: An explicit elementary proof of no Landau–Siegel zeros](https://arxiv.org/html/2610.30476)
6. [Reilly: siegel-zeros-audit verification package](https://github.com/jmreilly1113/siegel-zeros-audit)
7. [openai/math repository](https://github.com/openai/math) (primary)
8. [OpenAI: Uniform exclusion of Landau–Siegel zeros (directory)](https://github.com/openai/math/tree/main/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026) (primary)
9. [Scientific American: The most exciting claims from OpenAI's heap of new proofs](https://www.scientificamerican.com/article/the-most-exciting-claims-from-openais-heap-of-new-proofs/)

Author: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- collection: [Analysis](https://newruntime.com/analysis.json): Open the latest authorial analysis.
- collection: [Sources](https://newruntime.com/sources/): See the original sources this archive cites.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)