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\). (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above. Read the assessments
In The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane \(\Re s\gt 7/8\), 30 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
Every finite-order Hecke L-function over F=\mathbb Q(\sqrt{-3}) has no zero in \Re s>7/8. The same holds for every Dirichlet L-function, including \zeta(s). A pole at s=1 for a principal character is allowed.
In The Quasi-Riemann Hypothesis (alternate 11/12 proof), 5 October 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
Every finite-order Hecke L-function over K has no zeros in the half-plane \Rea s>11/12. Thus every Dirichlet L-function, including \zeta(s), has no zeros for \Rea s>11/12.
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.
Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
DirichletSevenEighthsThe paper states
In The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane \(\Re s\gt 7/8\), 30 September 2026
Every finite-order Hecke L-function over F=\mathbb Q(\sqrt{-3}) has no zero in \Re s>7/8. The same holds for every Dirichlet L-function, including \zeta(s). A pole at s=1 for a principal character is allowed.
The words they share: 7/8, dirichlet, re, character, zero, function, zeta.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
DirichletSevenEighths.lean, the release lists it as a main result.
theorem LFunction_ne_zero_of_seven_eighths_lt_re {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) (hpole : ¬ (χ = 1 ∧ s = 1)) : _root_.DirichletCharacter.LFunction χ s ≠ 0 := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
HeckeSevenEighthsThe paper states
In The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane \(\Re s\gt 7/8\), 30 September 2026
Every finite-order Hecke L-function over F=\mathbb Q(\sqrt{-3}) has no zero in \Re s>7/8. The same holds for every Dirichlet L-function, including \zeta(s). A pole at s=1 for a principal character is allowed.
The words they share: 7/8, rational, hecke, zeta, re, character, zero, function, finite, sqrt, order.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
HeckeSevenEighths.lean, the release lists it as a main result.
theorem LFunction_ne_zero_of_seven_eighths_lt_re (χ : Character) {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) (hpole : ¬ (χ.residue = 1 ∧ s = 1)) : LFunction χ s ≠ 0 := by sorry This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
QuasiRiemannHypothesisThe paper states
In The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane \(\Re s\gt 7/8\), 30 September 2026
Every finite-order Hecke L-function over F=\mathbb Q(\sqrt{-3}) has no zero in \Re s>7/8. The same holds for every Dirichlet L-function, including \zeta(s). A pole at s=1 for a principal character is allowed.
The words they share: 7/8, zeta, re, zero, riemann, dirichlet, character, function.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
QuasiRiemannHypothesis.lean, the release lists it as a main result.
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
SiegelZerosThe paper states
In Uniform exclusion of Landau–Siegel zeros, 1 October 2026
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\ge3 satisfies
The words they share: log, dirichlet, absolute, primitive, real, zero, function, nonprincipal, conductor, beta, constant.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
SiegelZeros.lean, the release lists it as a main result.
theorem exists_absolute_real_zero_gap : ∃ c : ℝ, 0 < c ∧ ∀ (q : ℕ) [NeZero q], 3 ≤ q → ∀ χ : DirichletCharacter ℂ q, χ.IsPrimitive → χ ≠ 1 → (∀ a : ZMod q, (χ a).im = 0) → ∀ β : ℝ, 0 < β → β < 1 → χ.LFunction (β : ℂ) = 0 → c ≤ (1 - β) * Real.log (q : ℝ) := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
The file states one more theorem: dirichletRealZeroBound_.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
UniformSiegelZeroExclusion Model.lean, line 8MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
Their note: No gap for zeta/Dirichlet L (Mathlib objects). Hecke 7/8 clause rests on a custom WeakFEPair-defined L-function (LFunction := continuedLattice χ s / 6) whose identification with the Dirichlet series is not in the statement; 11/12 companion not stated separately (implied).
Definitions the group asks readers to compare with the paper: Hecke part: def LFunction (χ : Character) (s : ℂ) : ℂ := continuedLattice χ s / 6 with continuedLattice χ = HeckeTheta.latticeL (coefficients χ) (custom theta/WeakFEPair construction; custom structure Character with modulus, residue : MulChar (O ⧸ modulus) ℂ, unit_trivial, period); no lemma linking it to Σ χ(a) N(a)^{-s}
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).
“MATCHES”, in their words: The challenge statements state the headline as OpenAI wrote it.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
OpenAI’s own note on what its Lean covers
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)$.
Dirichlet $L$-function $7/8$ bound DirichletSevenEighths
Unreviewed AI draft: states part of a paper’s theorem. States the Dirichlet L-function case of the main theorem, for every modulus and character, with the pole of a principal character at s = 1 excluded. The Hecke case over Q(√−3) is a separate statement.
Finite-order Hecke $L$-function $7/8$ bound HeckeSevenEighths
Unreviewed AI draft: states part of a paper’s theorem. States the first assertion of the main theorem, the 7/8 half-plane for finite-order Hecke L-functions over Q(√−3), using definitions of these L-functions made in the challenge file. The Dirichlet and zeta cases of the theorem are separate statements.
Riemann zeta $7/8$ bound QuasiRiemannHypothesis
Unreviewed AI draft: states part of a paper’s theorem. States the case of the Riemann zeta function in the main theorem: no zero with real part above 7/8. The Dirichlet and Hecke cases of the same theorem are separate statements (DirichletSevenEighths, HeckeSevenEighths).
Uniform real-zero gap SiegelZeros
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the Landau–Siegel paper: an absolute constant c > 0 with (1 − β) log q ≥ c for every real zero β in (0, 1) of every primitive nonprincipal real Dirichlet L-function of conductor q ≥ 3.
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
DirichletSevenEighthsThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-pass” | Re-run through Comparator: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 3839 s; peak memory 6.6 GiB). | 10 October 2026 | Original report |
HeckeSevenEighthsTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 564 s; peak memory 6.6 GiB). | 10 October 2026 | Original report |
QuasiRiemannHypothesisThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-pass” | Re-run through Comparator: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 555 s; peak memory 6.6 GiB). | 10 October 2026 | Original report |
SiegelZerosTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-pass” | Re-run through Comparator: accepted. | 8 October 2026 | Original report |
Other people’s accounts of running proof-verification software, with links to their reports.
Joseph M. Reilly, Verification package for openai/math family 003, Uniform exclusion of Landau-Siegel zeros, 9 October 2026. Source
Official Comparator with nanoda accepts both SiegelZeros challenge theorems with only the three standard axioms, with the network blocked.
GTimG, records contributed by Nielstron, Akash Levy, Hailey Collet, Tim Gehrunger, others, GTimG/QuasiRiemannTracker: dashboard of verified quasi-Riemann zero-free bounds, 9 October 2026. Source
Tracker reports OpenAI’s 7/8 proof passed Palomar’s mechanical verifier locally, including Comparator with Lean, NanoDa and con-ron kernels.
tomoto0, tomoto0/quasi-riemann-hypothesis-7-8-verification: independent verification of family 003, 7 October 2026. Source
Rebuild of the zeta and Dirichlet nonvanishing statements reported clean with only standard axioms; Hecke statement not built.
Vinicius M. Pimenta, vinicius-pi/independent-quasi-rh-checks: finite checks of two arithmetic lemmas in the family 003 paper, 7 October 2026. Source
Vinicius M. Pimenta reports numerical checks of two arithmetic lemmas in finite cases.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
davegoldblatt, openai-zeta-proof-check, 7 October 2026. Source
Comparator printed that the solution is okay with the default kernel and again with the independent nanoda kernel on a challenge file the author wrote, all 2,924 modules compiled, and only the three standard axioms appear.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
From github.com/davegoldblatt/openai-zeta-proof-check, 6 October 2026. Source
davegoldblatt reports the Lean proof of zeta(s) not zero for Re(s) > 7/8 compiled (2,924 modules, no errors) and was accepted by comparator under the Lean kernel and by the independent nanoda kernel at commit adc7f12; axioms are propext, Classical.choice, Quot.sound; the paper itself was not reviewed.
From community.openai.com, 6 October 2026. Source
davegoldblatt reports the Lean FRO Comparator accepted OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re at commit adc7f12, with the independent nanoda kernel also accepting and only propext, Classical.choice and Quot.sound used; all 2,924 modules compiled; single run by an AI agent that checks the Lean proof, not the paper.
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
Zvi Mowshowitz, New Math from OpenAI, 9 October 2026. Source
Alex Kontorovich’s thread explains that the best known zero-free region thinned with height and that a fixed strip also removes Siegel zeros.
Michael Rubinstein, Working notes on the quasi-Riemann hypothesis papers, 9 October 2026. Source
Accessible guides to the 11/12 argument for zeta and the 7/8 argument for a whole family, plus a CM-curve adaptation whose 7/8 part is conditional.
Michael Rubinstein, Working notes on the quasi-Riemann hypothesis papers, 9 October 2026. Source
Background notes on Z[omega], residue symbols and the cubic theta function used in the 11/12 argument.
foocker, foocker/openaimath: Chinese reading index of the release, 9 October 2026. Source
A narrated Chinese video explainer of about 95 seconds, with synchronised subtitles and chapters, for the 30 September quasi-Riemann hypothesis paper.
OfficeChai Team, OpenAI Releases AI-Generated Proofs Of Quasi Riemann Hypothesis, Unique Games Conjecture & Hodge Conjecture For CM Abelian Varieties, 7 October 2026. Source
Claimed theorem: no zeros of any Dirichlet L-function with real part above 7/8; a companion gives a weaker 11/12 region.
OfficeChai Team, OpenAI Solves Quasi Riemann Hypothesis: Understand What It Means, 7 October 2026. Source
Explainer quotes 11/12 (about 0.917) as the boundary, which matches the companion proof rather than the main 7/8 result.
zoahdev, zoahdev/math (branch docs/chinese-reading-guide): catalogue checker and Chinese reading guide, 7 October 2026. Source
Chinese-language reading guide with a worked navigation example for the quasi-Riemann hypothesis family.
seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source
Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.
davegoldblatt, openai-zeta-proof-check, 7 October 2026. Source
The theorem also covers s = 1, where Mathlib assigns the zeta function a conventional value that Mathlib already proves nonzero, and Mathlib already proves non-vanishing for real part at least 1, so the new content is the strip 7/8 < Re(s) < 1.
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Hexagon, Hexagon: a repository for research in the mathematical sciences and theoretical computer science, 10 October 2026. Source
hexagon:2610.00178v1 (Shubhrajit Bhattacharya, from one GPT-6 Astra prompt, no human scrutiny) lists published RH/GRH-conditional results that need only the 7/8 zero-free half-plane taken from OpenAI’s quasi-Riemann manuscript.
Jizhou Guo, Follow-ups to the OpenAI mathematics release (papers, sources and Lean ancillary files), 10 October 2026. Source
Zero-free half-plane Re s > 11/12 for Hecke L-functions of nonzero angular type over Q(sqrt -3), extending the release’s method (8 October).
Akash Levy, akashlevy/qrh: zero-free half-planes below 7/8 (10499/12000) and a 23/24 zeta proof, 10 October 2026. Source
Zero-free half-plane Re s > 10499/12000 with Lean, Comparator and three kernels (author-side); independently rebuilt for the tracker.
DrMurphyIsIn, qrh-debruijn-newman, 9 October 2026. Source
A small repository claims a bound of 9/32 on the de Bruijn-Newman constant; this is the owner’s claim and has had almost no outside attention.
GTimG, records contributed by Nielstron, Akash Levy, Hailey Collet, Tim Gehrunger, others, GTimG/QuasiRiemannTracker: dashboard of verified quasi-Riemann zero-free bounds, 9 October 2026. Source
As of 10 Oct 2026 the tracker lists 683505193/781250000 = 0.8748866 (Hailey Collet), below OpenAI’s 7/8, as the best zero-free bound to pass its Lean, Comparator and multi-kernel checks.
Rasmus Lindahl, contributors, mrconter1/vibemathed, 8 October 2026. Source
PR 109 ‘Curator replies: quasi-RH Lean question, K3 products withdrawal’ (8 October).
Baiying Liu, Slightly-improved-zero-free-half-planes-for-the-quasi-Riemann-hypothesis, 8 October 2026. Source
A small repository claims a slightly smaller zero-free half-plane than the manuscript’s 7/8; this is the owner’s claim and has had almost no outside attention.
Argonaut-Math, argonaut-math-quasi-riemann-boundary, 8 October 2026. Source
A small repository claims a refinement from 7/8 to 3499999/4000000; this is the owner’s claim and has had almost no outside attention.
Baiying Liu, Slightly improved zero-free half-planes for the quasi-Riemann hypothesis, 8 October 2026. Source
Liu improves OpenAI’s 7/8 zero-free half-plane to 34999/40000 and then to about 0.874957 by varying the two parameters of the same argument, and reports Lean 4 formalisations of the new constants.
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Offer to write an explanationCompare one Lean statement with its paper: QuasiRiemannHypothesis, DirichletSevenEighths, HeckeSevenEighths, SiegelZerosSuggest a source attributionSuggest a change
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Landmark of the century”. The page says that nothing on it is verified.
Author not stated. Source
grwtsk, [AUDIT.00] Audit the formal trust surface of the OpenAI math release (issue 2), 9 October 2026. Source
The Lean zeta 7/8 theorem includes s = 1 using Mathlib’s totalised value, whereas the paper allows a pole there; the audit says an explicit bridge or disclosure is needed and calls it not a proof failure.
grwtsk, [AUDIT.00] Audit the formal trust surface of the OpenAI math release (issue 2), 9 October 2026. Source
The two Landau-Siegel routes have disjoint local module closures (201 and 67 modules) but share Mathlib; the Comparator config for them has nanoda disabled.
From github.com/jkbennitt/math-release-atlas, 9 October 2026. Source
The math-release-atlas shows a fixed caution on this family: the result is a zero-free region for real part above 7/8, a quasi-Riemann hypothesis, and not the Riemann Hypothesis.
tparker, Philip Weiss, Will Sawin, Nik Weaver, Pace Nielsen, mathworker21, Joshua P. Swanson, Timothy Chow, Daniel Soltesz, MathOverflow: how many of the released results went against the conventional wisdom?, 8 October 2026. Source
An answerer says the most surprising feature is that conventional techniques narrow the critical strip, with three proofs of such a zero-free region.
Frank Calegari, A Brief Digest of Some New OpenAI Results, 8 October 2026. Source
Says quasi-RH was more surprising than RH would have been and that GRH-conditional results may now be provable with only Dirichlet L-function input; no improvement yet for Stark-Odlyzko discriminant bounds, which need Dedekind zeta functions.
eigendash, eigendash/openai-math-visualised: numerical probes of seven result families, 8 October 2026. Source
The first 600 zeta zeros show no zero with real part above 7/8, but the author states this cannot test the theorem: the zero finder only finds zeros on the critical line, so the figure is a drawing of the claimed region, not evidence.
Scientific American (byline not recorded), The most exciting claims from OpenAI’s heap of new proofs, 8 October 2026. Source
Hector Pasten (PUC Chile) says the quasi-Riemann hypothesis is enough for many applications of the full hypothesis and that the Siegel-zero result settles that question for zeta and Dirichlet L-functions.
tomoto0, tomoto0/quasi-rh-audit-public: independent technical audit of the quasi-Riemann hypothesis paper, 7 October 2026. Source
No fatal error found in the paper, but central analytic steps were not independently reconstructed; verdict is ‘not independently verified’.
Frank Calegari, The OpenAI problem dump, 6 October 2026. Source
Update says the quasi-Riemann hypotheses are in the dump and also yield an Artin-type result, though not the Artin conjecture they listed.
Lean community, OpenAI releases solutions to hundreds of problems (117 messages, 6-10 Oct 2026), 6 October 2026. Source
Whidden: higher-moment improvements stall at 7/8 because the Eisenstein field’s odd order of roots of unity keeps characters quadratic.
Levent Alpoge, Post praising the quasi-Riemann and no-Siegel-zero results, 6 October 2026. Source
Says they had been telling people the strip was within reach; credits OpenAI’s papers with quasi-RH and no Siegel zeros.
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Theorem 1.1
In The Quasi-Riemann Hypothesis, 30 September 2026
Why this passage is shown
Theorem 1.1
In The Quasi-Riemann Hypothesis (alternate 11/12 proof), 5 October 2026
Why this passage is shown
Theorem 1
In Uniform exclusion of Landau–Siegel zeros, 1 October 2026
Why this passage is shown
Corollary 1.2
In The Quasi-Riemann Hypothesis (alternate 11/12 proof), 5 October 2026
Why this passage is shown
Corollary 1.2
In The Quasi-Riemann Hypothesis, 30 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, DirichletSevenEighths
Proof-verification report
MathVet, DirichletSevenEighths
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, DirichletSevenEighths
Proof-verification report
cert-machine, HeckeSevenEighths
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, HeckeSevenEighths
Proof-verification report
cert-machine, QuasiRiemannHypothesis
Proof-verification report
MathVet, QuasiRiemannHypothesis
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, QuasiRiemannHypothesis
Proof-verification report
cert-machine, SiegelZeros
Proof-verification report
MathVet, SiegelZeros
Lean statement
DirichletSevenEighths
Lean statement
HeckeSevenEighths
Lean statement
QuasiRiemannHypothesis
Lean statement
SiegelZeros