Uniform exclusion of Landau–Siegel zeros

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 'Uniform exclusion of Landau–Siegel zeros'. We prove the uniform exclusion of Landau–Siegel zeros. 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 ≥ 3 satisfies (1-\beta)\log q\ge c.

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