cs.LO — Logic in Computer Science
Formalizing the interpolation lemma of the openai/math Landau–Siegel paper and substituting it into a Comparator-accepted proof
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.