# Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 24 references that are in the map.
- First posted on arXiv 25 Mar 2025.

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

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020)
- [Formalization of a Stochastic Approximation Theorem](https://mlsanity.com/paper/2202.05959/) (2022)

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

- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)

## Abstract (arXiv)

Understanding and certifying the generalization performance of machine learning algorithms -- i.e. obtaining theoretical estimates of the test error from the training error -- is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, Rademacher complexity yields sharp, data-dependent bounds that apply well beyond classical VC-dimension theory. In this study, we formalize the generalization error bound by Rademacher complexity in Lean 4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from countable hypothesis classes (where measurability of suprema is straightforward in Mathlib) to separable topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under ℓ2 and ℓ1 regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.