Two kernels check OpenAI’s Lean proof on Siegel zeros

On October 6, OpenAI published openai/math, a repository of manuscripts with Lean formalizations. One entry accompanies the preprint “Uniform exclusion of Landau–Siegel zeros”. Its Lean statement says that there is an absolute constant c > 0 such that, for every modulus q ≥ 3, every primitive real Dirichlet character χ modulo q, and every real zero β of L(s, χ) with 0 < β < 1, we have (1 − β) log q ≥ c. The statement is quoted in full at the end of this note.

Before we build on a result, we kernel-check it, and we publish the check. This note is that check for OpenAI’s entry: what we checked, how, what it shows, and how to repeat it.

What we checked

The two theorems that OpenAI’s own checking configuration names, exists_absolute_real_zero_gap and dirichletRealZeroBound_proof, in the module OAI.NumberTheory.SiegelZeros.Main, at commit fd4aeeb2 (the head of the main branch when we fetched it, October 10), with the Lean 4.34.1 toolchain and the Mathlib release the repository pins. The configuration (lean/ComparatorChallenges/SiegelZeros.json) permits the three standard axioms propext, Classical.choice and Quot.sound, and leaves its option for a second kernel switched off.

We were not the first to check this entry. On October 9, Joseph M. Reilly published a verification package for it, siegel-zeros-audit (doi:10.5281/zenodo.23269528), at an earlier commit, adc7f12; between it and fd4aeeb2 the 311 files of the Siegel development, the challenge files and the build pins are unchanged. It ran the Lean FRO’s Comparator tool (leanprover/comparator) on Linux with the network blocked and nanoda switched on as the second kernel, which we did not do, and it goes further than this note: it formalizes the preprint’s own proof of its Lemma 3, reroutes the Lean proof through it, and checks several of the paper’s statements by exact computation at small cases. Its run and ours used the same nanoda commit, so on the second kernel the two are one implementation run twice, not two. Beside it, this note gives a second build on a different machine and operating system, two controls that a configuration allowing only the three standard axioms refuses, and a check of the whole environment the proof module loads.

Lean’s kernel

We built the proof from source. lake update applied the repository’s 23 compatibility patches to its dependencies and reproduced the committed lake-manifest.json exactly. Mathlib’s compiled files came from Mathlib’s binary cache. The 318 modules built here, OpenAI’s 306 and 12 that its patches add to a dependency, compiled with no errors, and Lean’s kernel checked each declaration in them as it was built.

Two short Lean files then did four things. The first printed the axioms of both theorems. It restated the two statements of OpenAI’s challenge file word for word and proved each by the corresponding theorem. It printed the fully elaborated types of the two theorems, and the second file printed the same types on the challenge side; the two sides matched byte for byte. Together, the restatements and the comparison show that the proved statements are the challenged ones. And the first file planted a control theorem proved by sorry.

Both theorems depend on exactly propext, Classical.choice and Quot.sound. Of the five declarations the first file prints axioms for, the control is the only one whose axioms include sorryAx.

A second kernel

Lean’s kernel trusts the compiled Mathlib files it loads. To check those too, we exported the proof with lean4export and checked the export with nanoda, an independent type checker for Lean written in Rust.

The dependency closure of the two theorems is 122,700 declarations, from Lean’s core library through Mathlib to OpenAI’s proof. nanoda checked all of them with only the three standard axioms permitted and any other axiom a hard error, and its own report of the axioms it admitted names exactly those three. The same configuration refuses two controls: the challenge file’s sorry versions of the two statements (refused for sorryAx), and Lean.reduceBool (refused for Lean.trustCompiler).

We also checked the whole environment the proof module loads, 725,869 declarations, with nanoda. That run needs Lean.trustCompiler permitted as well, because the environment contains declarations that use it; the closure of the two theorems does not.

What this shows, and what it does not

It shows that OpenAI’s Lean proof proves OpenAI’s Lean statement, under two independent kernel implementations, with the three standard axioms and nothing else. (nanoda’s configuration below turns on its fast arithmetic for natural number and string literals. These are not axioms; Lean’s own kernel accelerates the same literals.)

It does not show that the preprint’s mathematics is right as written, or that the Lean statement says what the preprint claims; that is a question for readers of the statement, and the statement is short. A human audit of an earlier OpenAI release makes the same point, that a successful kernel check establishes the proposition as encoded (Sienicki and Sienicki, arXiv:2608.14673). It does not check lean4export or nanoda themselves, which we trust at the commits named below. We ran both kernels on one Mac, and did not run Comparator, whose sandbox requires Linux; Reilly’s package did. At fd4aeeb2, the repository’s own metadata gives its review status as “unchecked”.

How to repeat it

The proof and Lean’s kernel:

git clone --filter=blob:none --no-checkout --sparse https://github.com/openai/math.git
cd math && git sparse-checkout set --cone lean
git checkout --detach fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb
cd lean
lake update        # applies the patches; lake-manifest.json comes back unchanged
lake exe cache get
lake build OAI.NumberTheory.SiegelZeros.Main ComparatorChallenges.SiegelZeros
lake env lean Audit.lean

Audit.lean, placed in math/lean:

import OAI.NumberTheory.SiegelZeros.Main

open OAI.SiegelZeros.WeightedTorusJets in
set_option pp.all true in
#check @exists_absolute_real_zero_gap

open OAI.SiegelZeros.WeightedTorusJets in
set_option pp.all true in
#check @dirichletRealZeroBound_proof

#print axioms OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap
#print axioms OAI.SiegelZeros.WeightedTorusJets.dirichletRealZeroBound_proof

def ChallengeStmt1 : Prop :=
    ∃ c : ℝ, 0 < c ∧
      ∀ (q : ℕ) [NeZero q], 3 ≤ q →
      ∀ χ : DirichletCharacter ℂ q,
        χ.IsPrimitive → χ ≠ 1 → (∀ a : ZMod q, (χ a).im = 0) →
        ∀ β : ℝ, 0 < β → β < 1 → χ.LFunction (β : ℂ) = 0 →
          c ≤ (1 - β) * Real.log (q : ℝ)

def ChallengeStmt2 : Prop :=
    ∃ c : ℝ, 0 < c ∧ ∀ (q : ℕ) [NeZero q], 3 ≤ q →
      ∀ χ : DirichletCharacter ℂ q,
        χ.IsPrimitive → χ ≠ 1 → (∀ a : ZMod q, (χ a).im = 0) →
        ∀ β : ℝ,
          (0 < β ∧ β < 1 ∧ DirichletCharacter.LFunction χ (β : ℂ) = 0) →
            c ≤ (1 - β) * Real.log (q : ℝ)

theorem audit_bridge1 : ChallengeStmt1 := OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap
theorem audit_bridge2 : ChallengeStmt2 := OAI.SiegelZeros.WeightedTorusJets.dirichletRealZeroBound_proof

theorem audit_control : ChallengeStmt1 := by sorry

#print axioms audit_bridge1
#print axioms audit_bridge2
#print axioms audit_control

The same two #check commands with import ComparatorChallenges.SiegelZeros print the challenge side’s types for the comparison.

The second kernel:

git clone https://github.com/leanprover/lean4export.git
cd lean4export && git checkout v4.34.0      # 076e8e5
echo 'leanprover/lean4:v4.34.1' > lean-toolchain && lake build && cd ..
git clone https://github.com/ammkrn/nanoda_lib.git
cd nanoda_lib && git checkout 3a24072 && cargo build --release && cd ..

cd math/lean
lake env ../../lean4export/.lake/build/bin/lean4export OAI.NumberTheory.SiegelZeros.Main -- \
  OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap \
  OAI.SiegelZeros.WeightedTorusJets.dirichletRealZeroBound_proof > closure.ndjson
../../nanoda_lib/target/release/nanoda_bin config.json

with config.json:

{
    "export_file_path": "closure.ndjson",
    "use_stdin": false,
    "permitted_axioms": ["propext", "Classical.choice", "Quot.sound"],
    "unpermitted_axiom_hard_error": true,
    "nat_extension": true,
    "string_extension": true,
    "print_success_message": true,
    "pp_to_stdout": true
}

nanoda’s output ends:

axiom propext {a b : Prop} : Iff a b → Eq a b

axiom Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} : r a b → Eq (Quot.mk r a) (Quot.mk r b)

axiom Classical.choice.{u} {α : Sort u} : Nonempty α → α

Checked 122700 declarations with no errors

The two controls use the same configuration with export_file_path pointed at their own exports:

lake env ../../lean4export/.lake/build/bin/lean4export ComparatorChallenges.SiegelZeros -- \
  OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap \
  OAI.SiegelZeros.WeightedTorusJets.dirichletRealZeroBound_proof > challenge.ndjson
lake env ../../lean4export/.lake/build/bin/lean4export Init -- Lean.reduceBool > reduceBool.ndjson

nanoda stops on each with Error: export file declares unpermitted axiom "sorryAx" and "Lean.trustCompiler" respectively.

On our machine the export was 1.3 GB and nanoda’s check took two minutes. Fetching the dependencies and the Mathlib cache used about 22 GB of disk.

The statement

From lean/ComparatorChallenges/SiegelZeros.lean at fd4aeeb2, where the proof is replaced by sorry:

theorem exists_absolute_real_zero_gap :
    ∃ c : ℝ, 0 < c ∧
      ∀ (q : ℕ) [NeZero q], 3 ≤ q →
      ∀ χ : DirichletCharacter ℂ q,
        χ.IsPrimitive → χ ≠ 1 → (∀ a : ZMod q, (χ a).im = 0) →
        ∀ β : ℝ, 0 < β → β < 1 → χ.LFunction (β : ℂ) = 0 →
          c ≤ (1 - β) * Real.log (q : ℝ)

The second theorem, dirichletRealZeroBound_proof, states the same bound with the three conditions on β bundled into one hypothesis.

The checks were run by Claude agents working under my direction.