Focused Lean dependency audit

Pinned OpenAI commit: fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb.

Result

A complete static OAI import closure from DirichletL/Nonvanishing.lean and DirichletL/Foundation.lean was fetched and scanned: 2,924 modules, 25,009,201 source bytes, zero fetch failures. Every fetched local module is under OAI.NumberTheory.DirichletL. A further 19 imported external-package modules were reconstructed from their pinned upstream commits plus this repository's patches, with every unified-diff context/removal checked against the upstream source; reconstruction had zero errors.

The comment/string-aware scans found no code-level sorry, admit, axiom, unsafe, implemented_by, extern, native_decide, native_omega, run_cmd, or initialization/elaboration-hook token in that OAI closure or those 19 patched external modules. This rules out these visible textual admission mechanisms within the scanned closure. It is not a Lean compiler or kernel certificate, nor a full semantic analysis of all theorem dependencies.

Definitions and external patches

The only local def LFunction with the simple basename is OAI.SevenEighths.HeckeFamily.LFunction, at Hecke/IdealBridge.lean:95. It is the expected new Hecke-family function, defined from the continued lattice sum divided by six, with a proof of equality to its ideal Dirichlet series for Re(s)>1. It does not redefine Mathlib's Dirichlet L-function.

Nonvanishing.lean:22 explicitly concludes nonvanishing of _root_.DirichletCharacter.LFunction; its zeta theorem at line 30 uses riemannZeta. No local definition or abbreviation of riemannZeta or root DirichletCharacter.LFunction was found. No such redefinitions or occurrences were found in the 19 relevant patched external modules either.

The project pins Mathlib to the official leanprover-community/mathlib4 commit d13f23b723b8a846827a245b89c10fc7d3f11612, consistently in lakefile and manifest. Relevant upstream Mathlib files were fetched at that pin: Mathlib/NumberTheory/LSeries/RiemannZeta.lean defines riemannZeta := hurwitzZetaEven 0; DirichletContinuation.lean contains the standard Dirichlet L-function definition and its modulus-one relation to zeta. A pinned API listing of lean/patches contains 24 patches and none named for Mathlib. No local lean/Mathlib shadow sources occur in the root tree prefix (which covers the alphabetically earlier Mathlib position before truncating within OAI). The inspected lakefile patch hooks do not patch Mathlib.

The two non-Mathlib, non-Lean imported package roots in the OAI closure are:

• PrimeNumberTheoremAnd.Wiener, upstream AlexKontorovich/PrimeNumberTheoremAnd at c39a751132c88b6e8080b74c74023fd95b3d8be0; its imported closure is four patched files.
• RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Rellich, upstream abenenson/rellich-kondrachov at 70f85d4c1bf99c6e7d61e8be4daa6f3664d08d23; its imported closure is fifteen patched files.

The corresponding patch files are sizeable (approximately 1.99 MB and 147 KB). The PNT patch contains many additions unrelated to the imported Wiener path. I audited the reconstructed imported modules, rather than assuming every patch is merely cosmetic or auditing every unrelated addition. These imported patched modules have no textual admissions/redefinition of the target functions. Their remaining imports are stock Mathlib modules. The entire transitive upstream Mathlib dependency graph was not scanned or compiled here.

Comparator and execution status

The comparator challenge-file sorry is intentional: it is the reference statement to match. QuasiRiemannHypothesis.json points at the solution module and permits only propext, Quot.sound, and Classical.choice, with no sorryAx permitted. The actual solution declaration has no additional theorem hypotheses besides Re(s)>7/8. The Dirichlet endpoint also has positive modulus and principal-pole exclusion.

At the original audit on 2026-10-09, the repository required leanprover/lean4:v4.34.1, while installed toolchains included 4.34.0 but not 4.34.1. The direct 4.34.0 executable ran and reported an aarch64 Linux release build. comparator, landrun, and lean4export were absent from PATH. Invoking the elan-managed lake --version attempted to write elan state and returned a read-only filesystem error. No target module compilation, #print axioms, or strict comparator command was run for the paper. No toolchain/dependency installation was attempted during that original audit.

Toolchain update, 2026-10-13: Lean 4.34.1 was installed through elan and made the default. lean --version reports the aarch64 release at commit 5045d0056413266e57c625dcd7c365b10e377c52; Lake reports 5.0.0-src+5045d00 (Lean version 4.34.1). The paper's pinned source directory also selects 4.34.1. A separate core-Lean smoke theorem compiled successfully and #print axioms reported no axioms. Existing project pins and older installed toolchains were retained. The toolchain mismatch is resolved; the paper's dependency build and strict comparator verification remain outstanding, and the three comparator tools are still absent from PATH. See verification evidence and the smoke source.

The root lakefile has configuration-time hooks that clone and patch eleven unrelated dependency repositories, plus post-update hooks for additional packages. I read that code rather than executing it during this source-only audit. A proper certificate run should use an isolated, reviewed environment with the exact toolchain and comparator tools. It should record theorem matching, permitted-axiom enforcement, and tool revisions.

Interpretation

This audit found no visible admitted assumption or target-definition substitution on the fetched OAI and relevant patched-package import paths. It strengthens the evidence beyond the presence of a claimed formalization, but does not establish that the Lean sources elaborate or that the comparator accepts them. No mathematical error in the primary paper follows from the absence of a compiled certificate.

Artifacts and Sources

• lean_import_graph.json: full static OAI import graph and external roots.
• lean_static_audit.json: initial token scan and byte/module counts.
• lean_additional_token_audit.json: expanded scan. Its sole basename-LFunction hit is the legitimate namespaced Hecke definition above; its recorded blank source line is a regex leading-whitespace location artifact, not missing source.
• lean_external_static_audit.json: relevant patched external import closures, reconstruction status, and token scan.
• audit_lean_sources.py and audit_external_lean.py: reproducible source-download/static-audit scripts.
• sources/source_manifest.json: original and derived-source hashes, upstream pins and patch pins.
• Complete direct source URL catalogue.