What was already known
Classical zero-free regions approach Re(s)=1 with height. The manuscript builds on OpenAI’s fixed-half-plane claims for restricted field families, and on Kazhdan–Patterson metaplectic theory, to claim a uniform result for arbitrary number fields.
AI involvement
Dean Cureton and Jesse Thorner directed the research and mathematical judgments. They report AxiomProver participation in proofs, manuscript development and Lean formalization, including metaplectic constructions for general number fields.
The repository attributes proof generation and Lean development to AxiomProver under Cureton and Thorner. The current v2 Theorem 1.1 agrees with the 31/32 checkpoint; the older v1 mismatch is already resolved.
Importance
Gives a fixed-width zero-free half-plane across all number fields and the stated finite-order Hecke characters.
Limitations
This does not prove the Riemann hypothesis or a zero-free half-plane down to Re(s)=1/2. The formal theorem asserts a holomorphic continuation agreeing with Mathlib’s Dedekind zeta function for Re(s)>1; finite-order Hecke characters are represented as ray-class characters. The earlier fetched manuscript v1 stated 1−1/6000, while the newly retrieved v2 Theorem 1.1 states 31/32 and matches the pinned formal challenge. The registry metadata still cites v1; the public record deliberately links v2 and preserves that provenance discrepancy. This reconciles the numerical source versions without refuting v1. Mechanical checking and automated statement review do not establish outside mathematical acceptance; AIProofWatch has not audited the complete proof or rebuilt dependencies.
Technical verification
A completed rigorous check is documented for the scoped statement. Palomar: Lean, NanoDa and con-ron (reported): DedekindZetaZeroFree.main and heckeCorollary at 09afbb4ce6570c1615d58509dc197fc9f0956b7d, using the explicit analytic continuation/ray-class vocabulary and bound 31/32; only the three standard Lean axioms permitted.
Formal checking
Reported mechanical checking of the stated scope; not reproduced by AIProofWatch and not human peer review.
- Checker
- Palomar: Lean, NanoDa and con-ron (reported)
- Scope
- DedekindZetaZeroFree.main and heckeCorollary at 09afbb4ce6570c1615d58509dc197fc9f0956b7d, using the explicit analytic continuation/ray-class vocabulary and bound 31/32; only the three standard Lean axioms permitted.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-13
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. No sufficient account of a named human explaining the scoped central reasoning is established in this assessment. Missing disclosure is not evidence of little understanding.
Human follow-up work
- Submitted 13 Oct 2026; v2 dated 14 Oct 2026
Uses the OpenAI and Cureton–Thorner quasi-RH results for effective Chebotarev estimates and applications, including class-group torsion bounds and small generators. This is a human-authored application, not a check or explanation of either zero-free proof.
Christopher Frei, Efthymios Sofos, and Martin Widmer.
Correction and publication history
Primary statement, prior work, AI contribution and evidence scope reviewed on 15 October 2026 against the complete current catalog and revision state. New scoped contribution; ordinary notifying editor publication.
Read this published revision