Formally verified Collaborative

No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean

A Lean-formalized proof generated by Axiom Math's AxiomProver under two investigators' direction shows that for every number field $K$ the Dedekind zeta function $\zeta_K(s)$ has no zeros with $\Re s > 31/32$ .

Lab: Axiom Math
Model: AxiomProver
Field: Mathematics
Date: 2026-10-12
Human collaborators: Dean Cureton, Jesse Thorner

Sources

Original work

hexagonmath.orgHexagon: Cureton and Thorner, A quasi-Riemann hypothesis for Dedekind zeta functions↗GitHubAxiomMath/DedekindZetaZeroFree, the Lean formalization↗

What was found

The manuscript takes its strategy from OpenAI's Artin manuscript (2026-10-06-artin-primitive-root), which claims a zero-free strip $\Re s > 1 - 10^{-6}$ for finite-order Hecke $L$ -functions over cyclotomic fields containing the twelfth roots of unity, and extends it to every number field with the wider half-plane $\Re s > 31/32$ . It says the hardest part was formalizing Kazhdan and Patterson's metaplectic forms over number fields containing the twelfth roots of unity; abelian descent then reaches arbitrary number fields, and the Hecke corollary follows by factoring $\zeta_L$ for the cyclic extension $L/K$ cut out by the character. For $K = \mathbb{Q}$ the half-plane is narrower than the $7/8$ that 2026-10-06-quasi-riemann-hypothesis claims for the Riemann zeta function, but the result covers every number field and, unlike the OpenAI manuscripts it builds on, carries a third-party registration. The Lean statement is anchored on Mathlib's own NumberField.dedekindZeta: it asserts a function holomorphic away from $s = 1$ that agrees with $\zeta_K$ for $\Re s > 1$ and does not vanish for $\Re s > 31/32$ , which by uniqueness of analytic continuation is the continued zeta function. The repository credits code adapted from openai/math, Tau Ceti and LeanPool, and vendors a class field theory development from the Palomar archive. A corollary extending the half-plane to every finite-order Hecke $L$ -function over $K$ , wherever it is holomorphic, is also formalized and registered, against a definition of ray class characters written in the challenge file.

Novelty check

Read the Hexagon record (hexagon:2610.00200, versions 1 and 2, both dated 2026-10-12), the manuscript's abstract, first page and Section 15, the repository README, formalization.yaml and Challenge file on 2026-10-16. The manuscript presents the result as following the openai/math Artin strategy, and its references include the classical zero-free regions for Hecke $L$ -functions of Hinz and Coleman, which shrink toward $\Re s = 1$ with height. No earlier fixed zero-free half-plane for Dedekind zeta functions of arbitrary number fields was found in the registry, whose closest entries are the two OpenAI manuscripts named above.

Caveats and known objections

Graded formal for the zeta theorem only, on the Palomar registration, which replays the proof against the Challenge statement with Comparator, and on that statement, which uses only Mathlib's definition of the Dedekind zeta function in an existence-of-continuation form that determines the function uniquely. That is the anchoring 2026-10-06-quasi-riemann-hypothesis names as enough for formal on its own zeta statement, and it is why this entry differs from Palomar-registered results whose statements rest on their authors' own definitions. The repository's own review status is agent-reviewed rather than human-reviewed, and the Hexagon record labels the text a mix of human-written and AI-generated with human understanding of some parts only, so the formal grade certifies the theorem, not the manuscript's prose argument. The Hecke corollary is not covered by the grade and is kept out of the claim: it defines ray class characters in the Challenge file itself rather than through Mathlib; read here, the definition encodes characters of the narrow ray class group modulo $\mathfrak{m}$ , which covers every finite-order Hecke character, but nobody without a stake has confirmed it. The checked development compiles OpenAI's analytic number theory code and a vendored class field theory library rather than assuming them, and it does not check the OpenAI manuscripts' own $7/8$ or $1 - 10^{-6}$ statements. Autonomy is graded collaborative, the strictest defensible reading: the investigators directed the research and made the mathematical judgments while AxiomProver generated the proofs and the Lean, and the strategy itself came from OpenAI's manuscripts.

Machine-checked elsewhere

PalomarPALOMAR-2026-10-13-000010

AxiomMath/DedekindZetaZeroFree at 09afbb4ce657 · checked 2026-10-14

ProvedDedekindZetaZeroFree.mainDedekindZetaZeroFree.heckeCorollary

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

Permitted axioms are exactly propext, Quot.sound and Classical.choice.

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-16AddedEntered the registry graded Formally verified and Collaborative.

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

Graded formally verified for verification and collaborative for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-12-dedekind-zeta-quasi-riemann

BibTeX

@misc{whataifound-axiommath-2026-riemann,
  title        = {No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Axiom Math. Verification: Formally verified. Autonomy: Collaborative.},
  url          = {https://whataifound.org/finding/2026-10-12-dedekind-zeta-quasi-riemann}
}

Related findings

Formally verifiedErdős Problem 408: an unconditional normal order for the number of totient iterationsPlasma AI · 2026-10-19 Claimed719 manuscripts in 372 result families from an unreleased OpenAI modelOpenAI · 2026-10-06 ClaimedQuasi-Riemann hypothesis: no zeros of zeta or any Dirichlet L-function with real part above 7/8OpenAI · 2026-10-06

number-theory analytic-number-theory zero-free-regions lean formalization argument

← All mathematics findings in the registry