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 1 / 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.

Author comments: First 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.

Provenance statement

This work was produced by the contributor with substantial assistance from Anthropic’s Claude models, used in two ways. Planning and literature review (Claude, claude.ai, Claude Opus 5.5). I used Claude in a chat interface to identify what independent verification of the October 26, 2026 openai/math releases had already been done, locate prior replays and related formal developments, and draft a phased project plan with explicit scope limits. Claude’s web research located the third-party sources cited in Section [X]. I treated every fact from that research as unverified until it was checked against the files at the pinned commit; mismatches are noted in the text. Execution (Claude Code, [model]). Claude Code ran on [a WSL2 Ubuntu machine for Phase 0 and an AWS EC2 instance (instance type, Ubuntu 24.04, kernel version) for the replay runs]. It did the following under a written rule set that required pinned versions, complete logs, and a stop for my review at each phase boundary and on any anomaly: cloned the repositories and built the tools (Lean 4 [toolchain], Mathlib [rev], Comparator [SHA], lean4export [SHA], landrun [SHA], and nanoda in stock [SHA] and patched [SHA plus patch hash] builds) wrote the run and grep scripts executed the Comparator runs and recorded logs produced first drafts of the statement analysis and definitions inventory My role. I made the decisions at each review gate: the scope after finding prior nanoda runs treating a stack exhaustion in stock nanoda as a resource failure rather than a rejection the choice of VM [the assessment of the nanoda guard patch] I checked each factual claim in the paper against a log file, a file and line number, or a cited source, using a claims register included in the Zenodo archive. I wrote or revised the final text. What was not done. No part of this work assesses the mathematical correctness of the ETH or local smoothing proofs. Neither I nor the AI tools evaluated whether the bespoke analytic definitions are the right objects. Those questions are listed for domain experts.

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.CurrentNov 07, 2026