HEXAGONbeta

Formalizing the interpolation lemma of the openai/math Landau–Siegel paper and substituting it into a Comparator-accepted proof

Primarily AI-generated textHuman understanding: some partscs.LO — Logic in Computer Sciencemath.CA — Classical Analysis and ODEscs.CC — Computational Complexity

Contributed by Joseph Reilly

Version 2 / Nov 10, 2026 / CC BY 4.0

Abstract

OpenAI’s openai/math release includes a Lean formalization of “Uniform exclusion of Landau–Siegel zeros” (OpenAI, October 1, 2026). Its Comparator challenge has two checked theorems, whose statements we prove equivalent in Lean. OpenAI proves them by two routes, neither through the paper’s proof of Lemma 3. The catalogued main result, exists_absolute_real_zero_gap, gets its spanning step from a local Bézout argument and does not use OpenAI’s Corollary 4 theorem. The second theorem, dirichletRealZeroBound_proof, proves Corollary 4 by a multiplicity estimate. We formalized the paper’s proofs of Lemma 3 and Corollary 4 in Lean. By reading, the Lean statements match the paper’s, and the declarations use only the axioms propext, Classical.choice and Quot.sound. A +2/-1 substitution puts the paper’s Corollary 4 into dirichletRealZeroBound_proof. Comparator accepts the result with both kernels at openai/math fd4aeeb under a deny list of all 45 socket address families, and that theorem’s closure no longer contains the three named OpenAI lemmas. Our replay of the corpus agrees with an independent replay on all 402 configurations where both have a verdict.

Provenance statement

This work was produced with substantial assistance from Anthropic’s Claude models. Claude Code wrote the Lean files in lean-checks/, the run scripts in wsl-comparator/ and src/, the ledger builders and check.py, and the drafts of Sections 2–7; every tracked file in those places has at least one commit with a Co-Authored-By: Claude trailer. Claude Code also wrote the reading notes in results/2026-10-27-readings/, which record its readings before mine. Claude in chat (claude.ai) did the planning and wrote the prompts, gave the Lemma 3 and Corollary 4 statement comparison that preceded my reading, and helped draft public posts. All runs used a WSL2 Ubuntu machine (kernel 5.15.167.4) with Lean 4.34.1, Mathlib d13f23b, Comparator d03acab, lean4export 076e8e5 and nanoda 3a24072; results from unofficial nanoda builds are reported separately. I directed the work, approved each step, and performed the seven statement readings and the reviews of the reasoning points behind them, each signed off in docs/log.md. I wrote the content of the abstract, the introduction, Section 8 and Section 10 as point lists, and Claude Code drafted the text from them. I checked every reference against its source. No specialist in analytic number theory or transcendence has reviewed the mathematics. I take full responsibility for the content, including all text and code produced with AI tools.

Tools used

Anthropic
Claude OpusVersion 5.5
Lean
Lean

References

  1. ammkrn. nanoda_lib. 2026. Author given as the GitHub account name. GitHub repository ammkrn/nanoda_lib, commit 3a2407216ee84a75f9e1aead6803d0578be06ae7 (2026-09-22)link
  2. William D. Banks. On the OpenAI proof that Landau–Siegel zeros do not exist. 2026. arXiv:2610.15483 v1, 11 October 2026DOI
  3. Alexander Bastounis; Fabian Circelli; Anders C. Hansen. Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs. 2026. arXiv:2610.08144 v1 [math.AP], 6 October 2026link
  4. S. Fischler. Interpolation on algebraic groups. Compositio Mathematica, vol. 141, no. 4, pp. 907–925. 2005DOI
  5. grwtsk. [AUDIT.26] Reproduce manuscript PDFs and bind paper statements to exact Lean declarations. 2026. Author given as the GitHub account name. grwtsk/openai-math issue #29, opened 2026-10-09; comment 6296359378 (2026-10-20)link
  6. grwtsk. [AUDIT.35] Independently audit the uniform Landau–Siegel real-zero gap. 2026. Author given as the GitHub account name. grwtsk/openai-math issue #40, opened 2026-10-09; comments 6087525965 (2026-10-09) and 6431288875 (2026-10-27 UTC)link
  7. Lean FRO. Comparator. 2026. GitHub repository leanprover/comparator, tag v4.34.0, commit d03acab154d269c06e60e4de7e4cc85deebff94b (2026-09-14)link
  8. leanprover. Lean 4. 2026. Author given as the owning GitHub organization. GitHub repository leanprover/lean4, version v4.34.1, commit 5045d0056413266e57c625dcd7c365b10e377c52 (2026-09-24)link
  9. leanprover. lean4export. 2026. Author given as the owning GitHub organization. GitHub repository leanprover/lean4export, tag v4.34.0, commit 076e8e57707e813375e8f9da8bf989799ace9680 (2026-09-14)link
  10. leanprover-community. Mathlib. 2026. Author given as the owning GitHub organization. GitHub repository leanprover-community/mathlib4, commit d13f23b723b8a846827a245b89c10fc7d3f11612 (2026-09-24)link
Show all 23 referencesShow fewer references
  1. Neal McBurnett. OAI.SquareDifference.source_ordered_contraction overflows the stack on the current master. 2026. nanoda_lib issue #62, opened 2026-10-23link
  2. Neal McBurnett. openai-math-lean-tooling. 2026. GitHub repository nealmcb/openai-math-lean-tooling, commit 1ca7ff2a0280760783ee2b198c0d6f2a1cfeaba4 (2026-10-25)link
  3. Neal McBurnett. Stack overflow, then ``index exceeds 31-bit capacity'' panic, in \textttwhnf / \texttttry_reduce_nat on a small set of declarations that Lean's kernel checks in seconds. 2026. nanoda_lib issue #55, opened 2026-10-15; comment 6293743601 (2026-10-20)link
  4. Neal McBurnett. Three openai/math configurations need a deeper stack on the current master than on the earlier one. 2026. nanoda_lib issue #61, opened 2026-10-23; comment 6402528075 (2026-10-25)link
  5. OpenAI. openai/math. 2026. GitHub repository, commit adc7f1241b42e322a6451854ab7e4b4c146bf78a (2026-10-06)link
  6. OpenAI. openai/math. 2026. GitHub repository, commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb (2026-10-08 UTC)link
  7. OpenAI. The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re⁡s>7/8\operatorname{Re} s>7/8. 2026. Manuscript dated 30 September 2026, openai/math, \nolinkurlpreprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf, sha256 8fe93046\ldots, identical at commits adc7f12 and fd4aeeblink
  8. OpenAI. Uniform exclusion of Landau–Siegel zeros. 2026. Manuscript dated October 1, 2026, openai/math, \nolinkurlpreprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026/paper.pdf, sha256 fab9f6e8\ldots, identical at commits adc7f12 and fd4aeeblink
  9. Reilly, Joseph M. Comparator and nanoda replay of the openai/math Lean corpus at fd4aeeb, with statement checks for family 003. 2026. Zenodo, version corpus-replay-2026-10-20, 2026-10-20DOI
  10. Reilly, Joseph M. Verification package for openai/math family 003, Uniform exclusion of Landau–Siegel zeros: comparator + nanoda replay, Lean formalization of the paper's Lemma 3, rerouted proof, exact small-N checks. 2026. Zenodo, version reviewer-packet-v1, 2026-10-09DOI
  11. Reilly, Joseph M. Verification package for openai/math family 003, Uniform exclusion of Landau–Siegel zeros: comparator + nanoda replay, Lean formalization of the paper's Lemma 3, rerouted proof, exact small-N checks (preliminary). 2026. Zenodo, version reviewer-packet-v2-preliminary, 2026-10-20DOI
  12. Reilly, Joseph M. Verification package for openai/math family 003, Uniform exclusion of Landau–Siegel zeros: machine-checked complement to existing human write-ups (comparator + nanoda, Lean Lemma 3, explicit constant). 2026. Zenodo, version reviewer-packet-v3, 2026-10-21DOI
  13. Reilly, Joseph M. Verification package for openai/math family 003, Uniform exclusion of Landau–Siegel zeros: machine-checked complement to existing human write-ups (comparator + nanoda, Lean Lemma 3, explicit constant). 2026. Zenodo concept DOI (all versions); resolves to the latest version, reviewer-packet-v3DOI

Version history

  1. v1 · 20 pagesSubmitted by Joseph ReillyFirst version. Replay logs, tool pins, configurations, and checksums are archived at Zenodo, doi:10.5281/zenodo.23695266. Prepared with substantial assistance from Claude (Anthropic) via Claude Code; transcripts are included as supplementary material. This work reports what the formal statements and kernel runs show and makes no claim about the mathematical correctness of the underlying proofs.SupersededNov 07, 2026
  2. v2 · 20 pagesSubmitted by Joseph ReillySubmitted as a new versionCurrentNov 10, 2026