Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

Yuanhe Zhang, Jason D. Lee, Fanghui Liu

TL;DR

This work delivers the first end‑to‑end Lean 4 formalization of statistical learning theory anchored in empirical process theory, building a comprehensive toolbox for Gaussian analysis and Dudley’s entropy integral from scratch. It defines and proves a localized empirical‑process framework, enabling sharp rates for least‑squares regression and high‑dimensional l1 regression, with formal machinery such as Gaussian Lipschitz concentration and entropy integration. The results are implemented in a large Lean 4 codebase (~30k lines) through a human‑AI collaboration, demonstrating scalable formal verification and reusable foundations for future ML theory. By making implicit probabilistic and topological assumptions explicit and machine‑checked, the work advances rigorous theoretical analysis for modern ML systems and opens avenues for automated reasoning in statistical learning.

Abstract

We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration, the first formalization of 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 available at https://github.com/YuanheZ/lean-stat-learning-theory

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

TL;DR

This work delivers the first end‑to‑end Lean 4 formalization of statistical learning theory anchored in empirical process theory, building a comprehensive toolbox for Gaussian analysis and Dudley’s entropy integral from scratch. It defines and proves a localized empirical‑process framework, enabling sharp rates for least‑squares regression and high‑dimensional l1 regression, with formal machinery such as Gaussian Lipschitz concentration and entropy integration. The results are implemented in a large Lean 4 codebase (~30k lines) through a human‑AI collaboration, demonstrating scalable formal verification and reusable foundations for future ML theory. By making implicit probabilistic and topological assumptions explicit and machine‑checked, the work advances rigorous theoretical analysis for modern ML systems and opens avenues for automated reasoning in statistical learning.

Abstract

We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration, the first formalization of 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 available at https://github.com/YuanheZ/lean-stat-learning-theory
Paper Structure (36 sections, 13 theorems, 43 equations, 2 figures, 1 table)

This paper contains 36 sections, 13 theorems, 43 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. SLT from Natural Language to Lean 4
  3. Statistical learning theory for generalization
  4. Formalization Gaps
  5. Formulation details and challenges
  6. High-Dimensional Gaussian Analysis Toolbox
  7. ii. Gaussian Poincaré Inequality:
  8. iii. Density Arguments:
  9. Dudley's Entropy Integral Bound
  10. Application: Least Squares Framework
  11. Problem Setup.
  12. Localization.
  13. Main Results.
  14. Linear Regression
  15. High-Dimensional l1 Regression
  16. ...and 21 more sections

Key Result

Theorem 3.1

Let $\bm{X}= (X_1\,,...\,,X_n)$ be a vector of $n$ independent random variables and $Z=f(\bm{X})$ be a square-integrable function of $X$. Denote $E^{(i)}$ as the conditional expectation conditioned on $(X_1\,,...\,,X_{i-1}\,,X_{i+1}\,,...\,,X_n)$. Then,

Figures (2)

  • Figure 1: Lean formulation for Localized Empirical Process Framework. It includes the blue part for the capacity control and the red part for concentration. The colored zone indicates the major results in the chapters of wainwright2019high (High Dimensional Statistics, HDS) and Boucheron2013concen (Concentration Inequality, CI).
  • Figure 2: The dependency graph of our formalizations. All the contents in the graph have not been implemented in Lean 4 before.

Theorems & Definitions (13)

  • Theorem 3.1: i. Efron-Stein's Inequality, Theorem 3.20 in Boucheron2013concen
  • Corollary 1
  • Theorem 3.2
  • Lemma 1
  • Theorem 3.3: iv. Gaussian LSI, Theorem 5.4 of Boucheron2013concen
  • Theorem 3.4: v. Tensorization, Theorem 4.22 of Boucheron2013concen
  • Theorem 3.5: vi. Gaussian Lipschitz Concentration, Theorem 5.6 of Boucheron2013concen
  • Theorem 3.6: Dudley's Entropy Integral Bound
  • Theorem 4.1: Master error bound, Theorem 13.5 of wainwright2019high
  • Theorem 4.2
  • ...and 3 more