Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
This work provides a reusable formal foundation for machine learning theory, addressing implicit assumptions in textbooks and enabling future developments, though it is incremental in formalizing existing theory.
The authors tackled the lack of formal verification in statistical learning theory by developing the first comprehensive Lean 4 formalization, including Gaussian Lipschitz concentration and Dudley's entropy integral theorem, and applied it to achieve a sharp rate in least-squares regression.
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