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

arXiv: https://arxiv.org/abs/2602.02285 · HTML: https://mlsanity.com/paper/2602.02285/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 29 references that are in the map.
- First posted on arXiv 2 Feb 2026.

## Builds on (most cited first, 11 of 11)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Reconciling modern machine learning practice and the bias-variance trade-off](https://mlsanity.com/paper/1812.11118/) (2018)
- [Benign Overfitting in Linear Regression](https://mlsanity.com/paper/1906.11300/) (2019)
- [The generalization error of random features regression: Precise asymptotics and double descent curve](https://mlsanity.com/paper/1908.05355/) (2019)
- [Benign overfitting in ridge regression](https://mlsanity.com/paper/2009.14286/) (2020)
- [The merged-staircase property: a necessary and nearly sufficient condition for SGD learning of sparse functions on two-layer neural networks](https://mlsanity.com/paper/2202.08658/) (2022)
- [Intermediate Layer Optimization for Inverse Problems using Deep Generative Models](https://mlsanity.com/paper/2102.07364/) (2021)
- [Dynamical Decoupling of Generalization and Overfitting in Large Two-Layer Networks](https://mlsanity.com/paper/2502.21269/) (2025)
- [Survey on Algorithms for multi-index models](https://mlsanity.com/paper/2504.05426/) (2025)
- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization](https://mlsanity.com/paper/2403.11437/) (2024)

## Built on by (most cited first, 5 of 5)

- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries](https://mlsanity.com/paper/2605.07147/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [The Attribution Impossibility: No Feature Ranking Is Faithful, Stable, and Complete Under Collinearity](https://mlsanity.com/paper/2605.21492/) (2026)
- [GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research](https://mlsanity.com/paper/2609.36663/) (2026)

## Abstract (arXiv)

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.