Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
Yuanhe Zhang, Jason Lee, Fanghui Liu
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 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 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, resulting in approximately 30,000 lines of human-verified Lean 4 code produced over 500 hours of supervised development. 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 for future developments in machine learning theory. The code is provided in the supplementary materials.
BibTeX
@inproceedings{
zhang2026aislt,
title={{AI}4{SLT}: Empirical Processes in Lean 4 for Formal Statistical Learning Theory},
author={Yuanhe Zhang and Jason D. Lee and Fanghui Liu},
booktitle={Forty-third International Conference on Machine Learning},
year={2026},
url={https://openreview.net/forum?id=dfqmQ9WhCP}
}