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

Yuanhe Zhang; Jason D. Lee; Fanghui Liu

Source-linked AI summary

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

Yuanhe Zhang, Jason D. Lee, Fanghui Liu

arXiv:2602.02285v2Feb 2, 2026cs.LGcs.CLmath.ST

TL;DR

Modern statistical learning theory proofs are difficult to review and lack structured, machine-readable Lean 4 libraries for core techniques. This paper formalizes empirical-process-based SLT in Lean 4 through human-AI collaboration, developing Gaussian concentration and Dudley entropy tools and applying them to regression. The resulting framework obtains sharp, near-minimax rates for linear and ℓ1-constrained regression.

Problem
Complex SLT proofs strain human verification, while core techniques remain underdeveloped as structured, machine-readable Lean 4 libraries.
Method
The paper builds Lean 4 formalizations of Gaussian Lipschitz concentration and Dudley’s entropy integral bound through structured human-AI collaboration.
Results
The unified localized-empirical-process framework achieves sharp rates up to minimax level for linear and ℓ1-constrained regression.
Takeaways & Limitations
The verified Lean 4 toolbox provides a reusable foundation for formalizing modern statistical learning theory.
Takeaways & Limitations
Successful type-checking can conceal false statements when formalized goals are mis-specified, requiring explicit consistency verification.

Abstract

from arXiv · show

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.

1. Introduction

The section argues that increasingly intricate SLT proofs strain human verification while Lean 4 can provide machine-checkable correctness and a queryable foundation for scalable analysis. It introduces an end-to-end formalization covering concentration, entropy integrals, least-squares regression, and human–AI development.

Motivation: Increasingly complex theoretical analyses make intermediate lemmas, logical dependencies, and applicable techniques difficult to verify at scale.Modern proofs draw on advanced mathematics and statistical-physics-inspired tools.
Motivation: Lean 4 formalization supplies machine-checkable correctness guarantees and a structured, queryable library for scalable automated analysis.The section presents formalization as more than rigor: it is a foundation for theoretical analysis of machine-learning systems.
Contributions: The project develops SLT infrastructure from scratch across measure-theoretic probability, analysis, and empirical-process tools through human–AI collaboration.Its dependency structure follows representative components from Wainwright (2019) and Boucheron et al. (2013).
Contributions: The formalization includes complete Gaussian Lipschitz concentration infrastructure spanning Efron-Stein, Gaussian Poincaré, density arguments, and Gaussian logarithmic Sobolev inequalities.The Gaussian LSI is described as foundational in high-dimensional probability with applications beyond learning theory.
Contributions: It provides the first Lean 4 formalization of Dudley’s entropy integral theorem for sub-Gaussian processes, including chaining and metric-space covering and packing numbers.The theorem bounds an expected stochastic-process supremum using an integral involving metric entropy.
Applications and development: The work applies a unified localized empirical-process framework to least-squares, linear, and ℓ1-constrained regression, obtaining sharp rates up to minimax level.The development was completed through approximately 500 hours of supervised human–AI work and comprises approximately 30,000 lines of Lean 4 code.

2. SLT from Natural Language to Lean 4

The section presents empirical process theory as a geometric framework for uniform convergence and sharp learning guarantees, then identifies the advanced concentration and localization machinery missing from Lean 4. It positions the project’s comprehensive formalization as closing this gap while making suppressed assumptions and proof steps explicit.

SLT framework: Empirical process theory unifies generalization guarantees by exploiting the geometry of hypothesis and loss-function classes.The framework controls uniform convergence through empirical processes indexed by excess loss classes.
SLT framework: Concentration bounds control empirical-process fluctuations, while localization and complexity measures determine the critical radius δ⋆.Localized Gaussian and Rademacher complexities connect to metric entropy through covering numbers and Dudley’s entropy integral.
SLT framework: The resulting fixed-point characterization recovers sharp minimax rates in parametric settings and extends naturally to nonparametric models.Complexity accumulates across scales until the smallest solution defines δ⋆.
Formalization gap: Lean 4’s existing formalization lacks the advanced Gaussian concentration, covering-number, chaining, localized-complexity, and critical-radius machinery required by localized empirical-process analysis.Earlier work using whole-class Rademacher analysis provides looser rates and limited applications.
Formalization contribution: The project bridges this gap through comprehensive Lean 4 formalization that makes measurability, topological assumptions, almost-sure versus pointwise distinctions, and compressed proof steps explicit.The effort is described as going beyond mechanical translation and requiring careful proof engineering.

3. Formulation details and challenges

The section details a Lean 4 formalization of Gaussian Lipschitz concentration and Dudley’s entropy integral bound, emphasizing reusable infrastructure and explicit modeling and proof-engineering challenges. It develops an end-to-end Gaussian analysis toolbox while addressing assumptions and constants made implicit in textbook treatments.

3. Formulation details and challenges: The formalization covers Gaussian Lipschitz concentration and Dudley’s entropy integral bound, presenting natural-language theorems alongside Lean 4 implementations.The authors explicitly discuss modeling and proof-engineering challenges for each result.
3.1. High-Dimensional Gaussian Analysis Toolbox: The Gaussian analysis toolbox builds a reusable end-to-end pipeline from disparate, nontrivial analytic methods supporting HDS and SLT.The pipeline is represented as the red part of Figure 2.
3.1. High-Dimensional Gaussian Analysis Toolbox: A universal transfer lemma handles distinct coordinate distributions by showing that resampling one coordinate with a fresh independent sample preserves the joint distribution.The lemma supports 20+ uses across tower properties, Fubini-style swapping, and slice integration.
3.1. High-Dimensional Gaussian Analysis Toolbox: Theorem 3.3 formalizes that smooth compactly supported functions are dense in the Gaussian Sobolev space W1,2(γ⊗n).This density result extends Gaussian logarithmic Sobolev inequalities to C1 functions.
3.1. High-Dimensional Gaussian Analysis Toolbox: Lemma 3.4 formalizes Lipschitz mollification, producing smooth approximations that preserve the original Lipschitz constant and converge uniformly as ε decreases to zero.The implementation required substantial integration of functional analysis with measure-theoretic probability.
3.1. High-Dimensional Gaussian Analysis Toolbox: The Gaussian logarithmic Sobolev inequality is derived by formalizing a one-dimensional argument using Taylor limits, Rademacher sums, the central limit theorem, and Bernoulli LSI.Tensorization and entropy subadditivity then generalize the result to independent Gaussian coordinates.
3.2. Dudley’s Entropy Integral Bound: Dudley’s bound is formalized as a foundational bridge between covering numbers and complexity measures for theoretical results.The formalization makes integrability hypotheses and constants explicit rather than leaving them incomplete or implicit.

4. Application: Least Squares Framework

The section formalizes a least-squares framework for linear and ℓ1-constrained regression using localized capacity control through covering numbers. It establishes a critical-inequality/master-error-bound pipeline and applies it to linear regression, while extending the framework to the d > n ℓ1-constrained setting.

Framework: The framework covers linear regression and ℓ1-constrained regression, both relying on localized capacity control via covering numbers.The development builds on infrastructure from Section 3 and follows Wainwright (2019) and Raskutti et al. (2011).
Framework: Prediction error is controlled by shifting the hypothesis class, assuming star-shapedness, and solving a critical inequality linked to Gaussian complexity.The shifted class is F* := {f − f*: f ∈ F}, with 0 ∈ F* and αh ∈ F* for α ∈ [0, 1].
Framework: Theorem 4.1 formalizes the master error bound, while Theorem 4.2 supplies capacity control that reduces determining the error radius to bounding covering numbers.The resulting critical inequality becomes solvable through an entropy-integral upper bound.
Linear regression: For linear regression with n ≥ d, the framework yields a rate theorem parameterized by the design-matrix rank r.The theorem considers predictors f(·) = ⟨θ, ·⟩ and concludes a high-probability prediction-error bound for the least-squares estimator.
ℓ1-constrained regression: The ℓ1-constrained regression application extends the framework to d > n using Euclidean covering bounds for the ℓ1-convex hull.The covering lemma assumes column-wise normalization with ℓ2 norm at most √n and relies on Maurey’s argument.

5. Human-AI Collaborative Formalization

Across approximately 500 hours and 60 preserved task specifications, the authors identify structured specification, iterative refinement, and human verification as central to reliable Lean formalization. They report that explicit infrastructure and proof planning reduce first-attempt failures, while humans remain essential for detecting false statements.

5. Human-AI Collaborative Formalization: Approximately 500 hours of supervised development and 60 preserved task specifications yielded three methodological contributions and one critical observation.The section also classifies library declarations by required human intervention and provides a practical recipe.
5.1. Structured Specification Protocol: Structured TASK.md specifications reduce first-attempt failure rates from roughly 70% to roughly 15%.The protocol supplies explicit infrastructure pointers alongside the proof request.
5.1. Structured Specification Protocol: A structured specification states the exact Lean target and its self-contained natural-language meaning.This pairing clarifies both the formal signature and intended mathematical content.
5.1. Structured Specification Protocol: The protocol adds infrastructure pointers, a tactic-level proof plan, and hard boundaries for agent execution.Pointers identify locally available lemmas and file paths, while the plan translates informal mathematics into formalization steps.
5.2. Iterative Specification Evolution: Four specification iterations were required to formalize the Gaussian logarithmic Sobolev inequality density extension from C∞c to W 1,2.The iterations progressively resolved ambiguity around entropy convergence and the negativity of t log t.
5.2. Iterative Specification Evolution: The final specification’s shift trick and type-domain switch enabled the agent to succeed on its first attempt.Earlier retries with unchanged specifications essentially never succeeded because each failure exposed a distinct ambiguity.
5.3. Verification of Statement’s Consistency: The most dangerous failure is a type-checking proof of a false statement, which humans detected in three cases using explicit counterexamples.The cases included an invalid gap bound, an impossible disjunction, and an incorrect Riemann-rectangle upper bound.
5.4. Quantitative Breakdown: The Specified tier dominates the library, while tactical proof construction is less often the bottleneck than articulating compressed textbook arguments.Human-critical declarations include the non-delegable verification cases and some theorems whose initial statements were problematic.

6. Conclusion

The paper presents the first large-scale Lean 4 formalization of statistical learning theory, building verified infrastructure from scratch through human-AI collaboration and enabling further machine-learning theory formalization.

Conclusion: 30,000 lines of verified code constitute the first large-scale Lean 4 formalization of statistical learning theory.The infrastructure was built from scratch through human-AI collaboration.
Conclusion: The framework includes a high-dimensional Gaussian analysis toolbox for formal statistical learning theory.
Conclusion: The framework includes Dudley’s entropy integral toolbox, deepening mathematical understanding and opening the door to formalizing modern machine-learning theory.

A. List of Key Results

The formalization library contains more than 1000 theorems and lemmas. This section presents its major formalization results, with exact textbook references collected in Table 2.

A. List of Key Results: More than 1000 theorems and lemmas are included in the formalization library.The passage describes the library’s overall scale.
A. List of Key Results: The section focuses on presenting the major results of the formalizations.It introduces the purpose of the key-results list.
A. List of Key Results: Table 2 lists the key formalization results with exact references from textbooks.The table is identified as the location for the results and their references.

B. Dudley’s Formalization Proof Details · C. Lean 4 Formalization of Least Squares

The formalization develops Dudley’s chaining proof through dyadic nets, recursive projections, finite-to-countable extensions, and separability arguments. It then formalizes localized Gaussian complexity and makes explicit the technical hypotheses required for rigorous Lean statements.

B. Dudley’s Formalization Proof Details: DyadicNets constructs finite εk-nets at geometrically decreasing scales, with good nets satisfying |Tk| ≤ N(εk+1, s, d).Here εk = D · 2^-k and εk+1 = εk/2, linking net cardinality to the finer covering scale.
B. Dudley’s Formalization Proof Details: Recursive projection gives d(πk(u), πk+1(u)) ≤ εk, replacing the standard 3/2 factor and reducing the final chaining constant.The improvement propagates across levels, producing a noticeable reduction in the final constant.
B.1. Stage 1: Stage 1 bounds the expected supremum on the finest finite net by combining a coarsest-net base term with sub-Gaussian increment bounds across the hierarchy.The increment count is controlled through the cardinalities of finer nets and the good-net covering-number bound.
B.2. Stage 2: Stage 2 extends the finite-net bound to a countable dense sequence using a nonnegative shift, Fatou’s lemma, path continuity, and elimination of the vanishing tail.The shift transforms the potentially negative supremum YK into ZK ≥ 0, while the tail εK√log N(εK, s) tends to zero.
B.3. Stage 3: Stage 3 uses total boundedness to obtain a countable dense sequence and path continuity to identify the supremum over s with the countable supremum.Combining this identification with Stage 2 completes the passage from uncountable to countable suprema.
C.3. Observation: Lean exposes hypotheses often omitted in textbooks as essential conditions for rigorous extensions, including entropy-integral finiteness, continuity, integrability, and related technical assumptions.The formalization specifies exactly what must be verified when applying the theory to new settings.

C.1. Master Error Bound · D. Lean 4 Formalization of Covering of ℓ1-Convex Hull · E. Practical Recipe for Human-AI Collaborative Formalization

The formalization completes the master error bound and an entropy covering result for the ℓ1-convex hull, while the practical workflow emphasizes decomposed proofs and iterative cleanup for reliable human-AI collaboration.

D. Lean 4 Formalization of Covering of ℓ1-Convex Hull: The covering proof uses Maurey’s Empirical Method because the earlier combinatorial strategy yields complexity exponential in d.It represents hull points probabilistically, controls variance using column normalization, averages independent samples, and constructs a finite net.
D. Lean 4 Formalization of Covering of ℓ1-Convex Hull: Setting k = ⌈R^2/ε^2⌉ yields an ε-approximation, while the possible k-averages form a finite net because each sample has 2d + 1 possible values.The existence argument follows from the expected squared-distance bound R^2/k.
E.1. Decomposition Strategy: The workflow decomposes proofs into many leaf-level lemmas targeted at no more than 300 newly authored Lean lines per lemma.This improves reasoning allocation, isolates failures, increases reusability, and makes human review cheaper.
E.2. Anti-rewrite Instruction: The anti-rewrite instruction tells agents to change proofs only when confident they are wrong and to fix errors one by one.The paper reports this instruction produced the largest qualitative improvement observed during the project.
E.3. Iterative Cleanup Loop: After compilation, dedicated warning and dead-have cleanup passes are alternated until neither produces further edits.The loop addresses warnings, unused exploratory statements, and cascading issues while repeatedly verifying compilation.
E.3.1. WARNING CLEANUP and E.3.2. REMOVING UNUSED HAVE STATEMENTS: Warning cleanup removes unused variables rather than masking them with underscore prefixes, preserving genuine API design issues for review.The unused-have pass uses declaration-level checks, edits from bottom to top, and repeats until all declarations report no unused have statements.

F. Example Task Specifications

This section specifies extending the one-dimensional Gaussian logarithmic Sobolev inequality to continuously differentiable functions in W 1,2(γ). It formalizes the required Sobolev class, norm, smooth approximation, and compact-support inequality supporting that extension.

The target is the Gaussian logarithmic Sobolev inequality for every f ∈ C1(R) with f ∈ W 1,2(γ).
The formalized one-dimensional Gaussian Sobolev class requires both f and its derivative to belong to L2(γ).It is represented by MemLp f 2 γ ∧ MemLp (fun x 7→ fderiv R f x) 2 γ.
The strong Gaussian Sobolev norm squared combines the squared L2 norm of f with that of its derivative.The definition uses eLpNorm f 2 γ ˆ 2 + eLpNorm (fun x 7→∥fderiv R f x∥) 2 γ ˆ 2.
Every admissible continuously differentiable function admits smooth compactly supported approximants converging to it in the one-dimensional Gaussian Sobolev norm.The sequence is ContDiff and HasCompactSupport termwise, with GaussianSobolevNormSqReal (f - g k) tending to 0.
For compactly supported smooth functions, the formalized inequality bounds entropy by twice the squared gradient norm.The theorem states LogSobolev.entropy stdGaussianMeasure (fun x => (f x)ˆ2) ≤ 2 * R.
Optimal Proof for Formalization: The extension strategy passes the compact-support inequality to the limit using L2 convergence of functions and gradients and entropy lower semicontinuity.The entropy argument relies on L1 convergence of squared functions and convexity of ϕ(t) = t log t with Fatou-type arguments.

v2: Lower Semicontinuity of Entropy

The section formalizes the one-dimensional Gaussian Sobolev infrastructure needed to prove entropy lower semicontinuity. The proof combines smooth compact-support approximation, L1 subsequence convergence, and Fatou’s lemma applied to t log t.

Formalized infrastructure: The formalization defines the strong Gaussian Sobolev class using L2 integrability of a function and its derivative.The class requires MemLp f 2 γ and MemLp (fderiv R f) 2 γ.
Formalized infrastructure: It defines the strong Gaussian Sobolev norm squared as the sum of squared L2 norms of the function and derivative.The norm uses eLpNorm f 2 γ ^ 2 plus the corresponding derivative term.
Approximation: For continuously differentiable functions in the strong Gaussian Sobolev class, smooth compactly supported approximants converge in the one-dimensional Gaussian Sobolev norm.Each approximant is smooth and compactly supported, while the norm-squared error tends to zero.
Proof strategy: L1 convergence yields a strictly increasing subsequence that converges almost everywhere.The formalized theorem assumes measurable functions and eLpNorm-one convergence to zero, then produces pointwise convergence almost everywhere.
Lower semicontinuity of entropy: Entropy is lower semicontinuous under L1 convergence of nonnegative functions, proved by applying real-valued Fatou’s lemma to the convex integrand ϕ(t) = t log t.The argument passes to an almost-everywhere convergent subsequence and uses the integrand’s lower bound.

v3: Convergence of the Gradient Term in L2(γ)

The section formalizes density of smooth compactly supported functions in a one-dimensional Gaussian Sobolev space and derives convergence consequences for L2(γ). Under continuous differentiability, Sobolev-norm approximation yields convergence of the gradient term in L2(γ).

Gaussian Sobolev infrastructure: The formalization defines the squared Gaussian Sobolev norm as the sum of squared L2 norms of a function and its derivative.The definition uses eLpNorm f 2 γ ^ 2 and eLpNorm of fderiv R f under γ.
Approximation theorem: Every continuously differentiable f in the strong Gaussian Sobolev class admits smooth compactly supported approximants converging in squared Gaussian Sobolev norm.The sequence is continuously differentiable, compactly supported, and its approximation error tends to zero in the Gaussian Sobolev norm.
L2 convergence: Convergence to zero in squared Gaussian Sobolev norm implies convergence to zero in L2(γ).The formalized lemma states that eLpNorm (f - g k) 2 µ tends to nhds 0.
Convergence of the Gradient Term: The approximation sequence yields gradient convergence ∥∇f − ∇gk∥L2(γ) → 0, equivalently E[∥∇f(X) − ∇gk(X)∥2] → 0.This is the stated convergence of the gradient term obtained from the Gaussian Sobolev norm approximation.

v4: GLSI Extension to Strong Gaussian Sobolev Space

This extension formalizes density and convergence tools for the one-dimensional strong Gaussian Sobolev space, then establishes the compact-support Gaussian logarithmic Sobolev inequality and the ingredients needed for extension to continuously differentiable Sobolev functions.

Density and Sobolev convergence: A smooth compactly supported sequence converges to every continuously differentiable f ∈ W 1,2(γ) in squared Gaussian Sobolev norm.Each approximant is continuously differentiable and compactly supported, while GaussianSobolevNormSqReal (f - g k) tends to 0.
Density and Sobolev convergence: Squared Gaussian Sobolev convergence implies L2 convergence, L1 convergence of pointwise squares, and L2 convergence of gradients.The gradient implication additionally assumes differentiability, continuous gradients, and L2 integrability of the relevant derivatives.
Gaussian logarithmic Sobolev inequality: The one-dimensional Gaussian logarithmic Sobolev inequality is formalized for twice-differentiable compactly supported functions, with entropy of f^2 bounded by 2 times the squared derivative norm.The stated result applies under the CompactlySupportedSmooth assumption.
Extension proof strategy: The target statement concerns every continuously differentiable f ∈ W 1,2(γ), extending the compact-support inequality through Sobolev approximation and lower semicontinuity.The supplied target passage specifies the function class but does not include the final displayed inequality.
Extension proof strategy: The extension strategy uses continuity and the lower bound ϕ(t) = t · log(t) ≥ −1/e, L1-to-a.e. subsequences, and Fatou’s lemma for lower semicontinuity.The nonnegative shift by 1/e permits Fatou’s lemma even when integrals may equal +∞.