Théorie de l'apprentissage statistique en Lean 4 : Processus empiriques depuis les bases

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

February 2, 2026

papers.authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu

cs.AI

papers.abstract

Nous présentons la première formalisation complète en Lean 4 de la théorie de l'apprentissage statistique (SLT) fondée sur la théorie des processus empiriques. Notre infrastructure formelle de bout en bout implémente les contenus manquants dans la dernière bibliothèque Lean 4 Mathlib, incluant un développement complet de la concentration gaussienne lipschitzienne, la première formalisation du théorème de l'intégrale d'entropie de Dudley pour les processus sous-gaussiens, et une application à la régression des moindres carrés (creuse) avec un taux optimal. Le projet a été réalisé en utilisant un flux de travail collaboratif humain-IA, dans lequel les humains conçoivent les stratégies de preuve et les agents IA exécutent la construction tactique des démonstrations, aboutissant à une boîte à outils Lean 4 pour la SLT vérifiée par des humains. Au-delà de l'implémentation, le processus de formalisation expose et résout les hypothèses implicites et les détails manquants dans les manuels standards de SLT, imposant une compréhension granulaire, ligne par ligne, de la théorie. Ce travail établit une fondation formelle réutilisable et ouvre la porte à des développements futurs dans la théorie de l'apprentissage automatique. Le code est disponible à l'adresse https://github.com/YuanheZ/lean-stat-learning-theory

English

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