MVEI: A Reproducible Multi-Version Lean Verification Infrastructure for Large-Scale Formal Proof Auditing and Repository Diagnostics

MVEI: A Reproducible Multi-Version Lean Verification Infrastructure for Large-Scale Formal Proof Auditing and Repository Diagnostics Abstract The MVEI project develops a computational infrastructure for auditing Lean formalization repositories across heterogeneous compiler versions, dependency configurations, and project architectures. The infrastructure is intended to distinguish successful kernel verification from compilation failures, missing dependencies, unsupported command-line options, resource exhaustion, and mathematical obligations that remain unresolved. The reported audit covers repositories containing large collections of formal declarations, including projects based on different Lean versions and Mathlib releases. A preliminary execution identified 19 projects requiring further investigation or reexecution. This release documents the verification methodology, failure classification, reproducibility requirements, and proposed corrections. 1. Multi-Version Verification Architecture MVEI is designed to examine projects across different Lean compiler environments. It must respect each project's declared toolchain and dependency versions rather than assuming compatibility with a single contemporary Mathlib installation. Verification results are associated with the exact source revision, compiler version, dependencies, execution command, and process outcome. 2. Kernel Verification and Result Classification The infrastructure distinguishes between: - Successfully compiled declarations. - Declarations requiring additional axioms. - Source-level elaboration or type errors. - Missing modules and dependency failures. - Compiler invocation incompatibilities. - Stack exhaustion and resource-related termination. - Incomplete verification attempts. A successful process exit is necessary but not sufficient for a claim of mathematical independence from additional axioms. Each proof must also be assessed against its declared assumptions and the trust boundary of the Lean kernel. 3. Diagnostic Findings The reported preliminary audit identifies several technical obstacles. Lean 4.3.0 does not support the command-line "--json" option used by the existing verification procedure, preventing certain projects from reaching the intended source-level checks. Large generated Lean files encounter stack exhaustion or macro-expansion failures. Other projects exhibit missing imports, incompatible Mathlib environments, duplicate package declarations, or malformed source definitions. These failures must not automatically be interpreted as mathematical refutations. 4. Mathematical Consistency Auditing Beyond compilation, MVEI examines the logical compatibility of axiomatic structures. The reported analysis of indeterminate algebra identifies an inconsistency between standard ring multiplication and an axiom requiring multiplication by zero to equal one. A separate algebraic structure admits a conventional model involving an idempotent element in a product ring. These findings illustrate the distinction between a satisfiable algebraic theory and a contradictory extension of ordinary ring axioms. 5. Reproducibility and Provenance Each verification record should contain: - Repository identifier and immutable commit SHA. - Branch and source file. - Lean and Mathlib versions. - Exact invocation command. - Exit code, stdout, and stderr. - Execution resource limits. - Theorem name and declaration type. - Axiom dependencies. - Certificate or log checksum. 6. Security and Repository Isolation The infrastructure must separate public verification artifacts from private source repositories and restricted material. Historical exposure of private files or fixed identifying strings is treated as a provenance and repository-security issue, independent of mathematical verification. A fixed source string is not a cryptographic signature. 7. Research Scope MVEI is a formal verification and auditing infrastructure. It is not itself a proof of the mathematical conjectures represented by the repositories it examines. Its scientific contribution is the development of reproducible verification procedures and a transparent classification of proof status. Current Validation Status The reported audit remains incomplete. Nineteen projects require corrected execution, source repair, dependency restoration, or further diagnosis. Publication of a stable release should follow successful testing of the corrected verifier and preservation of the relevant execution records. Research Significance The project contributes to reproducible formal mathematics, proof engineering, software verification, and large-scale repository auditing. Its methodology may help researchers distinguish verified formal statements from unsupported claims, incomplete proofs, and infrastructure failures.