From Agents to Axioms: Verifier-Gated Lean Formalization for Statistical Learning Theory

This paper presents a verifier-gated acceptance workflow for agent-assisted Lean formalization, demonstrated on FormalSLT, a nontrivial Lean 4 / Mathlib statistical-learning-theory library. The contribution is not a new statistical-learning-theory theorem or a model benchmark; it is a reproducible PR-level protocol in which machine-written formalization edits are treated as untrusted proposals and admitted only through Lean build, proof-hygiene gates, and a blocking #print axioms audit. The submitted artifact contains 45 Lean modules, 20,080 source lines including FormalSLT.lean, 412 theorem/lemma declarations, and 107 showcase axiom traces covering VC, PAC-Bayes, Rademacher, Azuma, covering-number, and algorithmic-stability components. Over a 61h39m May 2026 run, theorem-scoped targets were dispatched through isolated worktrees and pull requests; the ledger records 67 opened PRs, 60 merged, and 7 closed or superseded. The accepted showcase theorems audit to {propext, Classical.choice, Quot.sound}. The result is a concrete acceptance layer for reliable scientific agents: agents may propose formalization state transitions, but the Lean kernel, CI, and axiom audit decide what lands.