The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s)>7/8

Lean formalization in OpenAI math repository (Result 003)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s)>7/8'. We prove that all finite-order Hecke L-functions over \mathbb Q(\sqrt{-3}) and all Dirichlet L-functions are zero-free in the half-plane \Re s\gt 7/8, with the principal pole at s = 1 allowed. In particular, the Riemann zeta function is zero-free in this half-plane, proving the quasi-Riemann hypothesis.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 003). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository