AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory

AI summary

Overview

• Research area: Formal verification of mathematics using the Lean 4 interactive theorem prover, applied to statistical learning theory (SLT) and machine learning theory, specifically the empirical process framework. The paper sits at the intersection of measure-theoretic probability, high-dimensional statistics, and proof engineering.
• Technical level: Advanced.
• Scope: The paper presents an end-to-end Lean 4 formalization of the empirical-process toolkit behind generalization bounds in SLT, plus a least-squares regression application and a human-AI workflow that produced roughly 30,000 lines of verified code.

What This Paper Is About

Statistical learning theory is built on long, technical proofs involving concentration inequalities and capacity/complexity control, and these proofs have grown difficult for humans to verify and reuse at scale. The core tools (concentration, covering numbers, chaining) also lack a structured, machine-readable library. The paper's goal is to build a machine-checked Lean 4 foundation for SLT grounded in empirical process theory, starting from basic measure-theoretic probability and analysis, and to demonstrate it on least-squares regression.

Key Contributions

1. A complete formalization of Gaussian Lipschitz concentration. The paper claims this is "the first formalization of the complete Gaussian analysis tools in any theorem prover," built as an end-to-end chain spanning the Efron-Stein inequality (Theorem 3.20 in Boucheron et al., 2013), the Gaussian Poincare inequality, density arguments, and the Gaussian logarithmic Sobolev inequality (LSI), with entropy subadditivity and tensorization.
2. The first formalization of Dudley's entropy integral theorem for sub-Gaussian processes in Lean 4. This required building covering numbers, epsilon-nets, metric entropy, dyadic chaining, and the telescoping decomposition of a stochastic process, along with two limit arguments (Fatou's lemma on finite nets, then extension to uncountable sets via path continuity).
3. A least-squares application framework via the localized empirical process. The formalization follows Wainwright (2019, Chapter 13) and is instantiated on linear regression and ℓ1-constrained (Lasso-style) regression, obtaining sharp rates up to minimax level, plus a standalone bound on covering numbers of Euclidean balls.
4. A human-AI collaborative formalization paradigm. Humans analyzed Mathlib's infrastructure, designed proof strategies, and decomposed theorems; the AI agent (Claude Code with Opus-4.5) executed the tactical proof construction. The process totaled approximately 500 hours of supervised development and all formalizations compiled without sorry or axiom.

Main Findings

• Formalization exposes hidden assumptions in textbooks. The authors report that the process resolves implicit assumptions and missing details in standard SLT texts, forcing explicit treatment of measurability, integrability, topological hypotheses, and almost-sure versus pointwise statements that natural-language proofs routinely suppress.
• Dudley's bound requires proof engineering across two integration formalisms. Lean 4 has a nonnegative improper integral ∫⁻ for ℝ≥0∞ and an interval integral for real-valued functions; the entropy integral is defined canonically in ENNReal with a real-valued wrapper used for Dudley's statement.
• The Dudley constant is made explicit. The formalized Theorem 3.8 states that for a normalized sub-Gaussian process with parameter σ > 0 on a totally bounded set of diameter at most D > 0, with finite entropy integral, the expected supremum is at most 12√2 · σ · ∫₀^D sqrt(log N(ε, s, d)) dε.
• Gaussian LSI underpins the concentration chain. The formalized LSI (Theorem 3.5, Theorem 5.4 of Boucheron et al., 2013) gives Ent(f²) ≤ 2 E[‖∇f(X)‖₂²], and the paper reports that the Lipsschitz concentration bound — P(|f(X) − E[f(X)]| ≥ t) ≤ 2 exp(−t²/(2L²)) — is proven via the Herbst argument, a Gronwall-type ratio bound, and Chernoff's bound.
• Mollification makes the density step explicit. A mollifier argument shows that for an L-Lipschitz function, sup_x |f_ε(x) − f(x)| ≤ L·C_ρ·ε, where C_ρ := ∫ ‖u‖₂ ρ(u) du < ∞, so f_ε → f uniformly.
• The master error bound is formalized. Theorem 4.1 (Theorem 13.5 in Wainwright, 2019) states P(‖f − f*‖²_n ≥ 16 t δ*) ≤ exp(−n t δ* / 2σ²) for t ≥ δ*, where δ* is the smallest positive solution to the critical inequality.
• Capacity control translates Gaussian complexity into an entropy integral. Theorem 4.2 gives G_n(F(δ)) ≤ (24√2 / √n) ∫₀^{2δ} sqrt(log N(ε, F(δ), ‖·‖_n)) dε.
• Linear regression rate. Theorem 4.3 states that with r := rank(X), P(‖f̂ − f*‖²_n ≤ C₁ σ² r / n) ≥ 1 − exp(−C₂ r) for constants C₁, C₂ > 0. The proof reduces the covering number to that of an ℓ2 ball of radius δ on ℝ^r, and uses Theorem 4.4: N(ε, B₂^ι(R), ‖·‖₂) ≤ (1 + 2R/ε)^ι (Vershynin, 2018, Corollary 4.2.11).
• Sparse regression rate setup. In the ℓ1-constrained (Lasso-equivalent) setting following Raskutti et al. (2011), Lemma 4.5 bounds N(ε, absconv₁(X/√n; R), ‖·‖₂) ≤ (2d + 1)^{⌈R²/ε²⌉} under column-wise normalization, and the paper reports obtaining δ* = O(sqrt{r/n}) in the linear case before applying Theorem 4.1.
• Position relative to prior Lean work. The authors note that Sonoda et al. (2025) formalized generalization bounds via Rademacher complexity with tools such as McDiarmid's inequality and Hoeffding's lemma, but controlled the empirical process over the entire function class, leading to looser rates and narrower applications. Other Lean 4 work in machine learning is cited in reinforcement learning theory (Zhang, 2025) and optimization (Li et al., 2024; Li et al., 2025a; Li et al., 2025b).
• A reusable measure-theoretic transfer lemma was highly reused. Formalizing coordinate-wise resampling (to handle distinct coordinate distributions) required measure rectangles, and the paper reports this lemma powered more than 20 usages across tower properties, Fubini-style swapping, and slice integrability.

Methodology in Plain English

The authors did not attempt to machine-check existing textbook proofs as written. Instead, they rebuilt the required probability and analysis machinery from scratch on top of Lean 4's existing libraries, following a dependency graph that covers the concentration side (in red in their Figure 2) and the capacity-control side (in blue in their Figure 1). The work was split between humans, who inspected what Mathlib already offered, chose proof strategies, and broke large theorems into manageable lemmas, and an AI coding agent (Claude Code with Opus-4.5), which produced the tactical proof scripts. The project overall involved approximately 500 hours of supervised development and approximately 30,000 lines of Lean 4 code, and the authors state that everything compiles without sorry or axiom. The paper reports the workflow as one demonstration of how large formalization efforts can be accelerated by pairing human design with AI execution.

Why This Matters

• Research impact: The paper argues that formalization addresses two bottlenecks in modern machine learning theory — verification at scale (tracking intermediate lemmas and logical dependencies in very long proofs) and untapped reusability (no structured, machine-readable library for concentration and covering arguments). The formalization becomes a reusable formal foundation that future developments in machine learning theory can build on.
• Real-world applications (as framed by the paper):
  • Least-squares and linear regression: the formalized framework produces a rate depending on the rank r of the design matrix, with a high-probability guarantee.
  • High-dimensional sparse regression / Lasso-style estimation: the ℓ1-constrained setting where d > n, using the ℓ1-ball class and Euclidean covering of the convex hull.
  • Machine-checked theory for generalization bounds: the concentration and capacity-control stack can support downstream generalization analyses of learning algorithms.
  • Training and pedagogy: the authors describe the formalization as a principled training ground for students, demanding mastery of the full technical stack of SLT rather than superficial familiarity.
• Industry relevance: The paper does not describe commercial deployments. Its industry relevance is stated in terms of scalable, automated theoretical analysis of machine learning systems, and the practical value of a machine-checkable correctness guarantee combined with a queryable, structured library of results. The code is released at https://github.com/YuanheZ/lean-stat-learning-theory under a CC BY 4.0 license.

Future Directions

• Extending beyond the current rate analysis. The formalized least-squares framework is demonstrated on linear and ℓ1-constrained regression; the paper presents this as a foundation for further theoretical developments rather than a finished library.
• Covering more of the modern SLT pipeline. The abstract frames this as the first comprehensive Lean 4 formalization grounded in empirical process theory, and describes it as opening the door for future developments in machine learning theory, implying that additional complexity measures (for example, Rademacher complexity in localized form) remain to be built out.
• Scaling the human-AI workflow. The project is described as one realization of accelerated formalization; the natural follow-up question is how far this human-strategy / AI-tactics division of labor extends to other large mathematical areas.
• Application to more complex model classes. The introduction motivates formalization by reference to double descent, benign overfitting, and single/multi-index models, which are not formalized here and would require further infrastructure.

Target Audience

This paper is most useful to researchers working on formal verification of mathematics and on the theory of machine learning, particularly those interested in Lean 4 libraries, empirical process theory, and high-dimensional statistics. It also targets graduate students and instructors in theoretical machine learning who want a rigorous, line-by-line training ground in SLT, and researchers or engineers interested in human-AI collaborative proof development at scale. Readers need comfort with measure-theoretic probability and concentration inequalities to follow the technical sections; the workflow and infrastructure discussion is accessible at a more general level.

Authors’ abstract

We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our en-to-end formal infrastructure implement the missing contents in latest Lean library, including a complete development of Gaussian Lipschitz concentration, Dudley's entropy integral theorem for sub-Gaussian processes, and an application to least-squares (sparse) regression with a sharp rate. The project was carried out using a human-AI collaborative workflow, in which humans design proof strategies and AI agents execute tactical proof construction, leading to the human-verified Lean 4 toolbox for SLT. Beyond implementation, the formalization process exposes and resolves implicit assumptions and missing details in standard SLT textbooks, enforcing a granular, line-by-line understanding of the theory. This work establishes a reusable formal foundation and opens the door for future developments in machine learning theory. The code is provided in https://github.com/YuanheZ/lean-stat-learning-theory.