Teoría del Aprendizaje Estadístico en Lean 4: Procesos Empíricos desde Cero

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

February 2, 2026

Autores: Yuanhe Zhang, Jason D. Lee, Fanghui Liu

cs.AI

Resumen

Presentamos la primera formalización integral en Lean 4 de la teoría del aprendizaje estadístico (SLT) basada en la teoría de procesos empíricos. Nuestra infraestructura formal de extremo a extremo implementa los contenidos faltantes en la biblioteca Mathlib más reciente de Lean 4, incluyendo un desarrollo completo de la concentración gaussiana de Lipschitz, la primera formalización del teorema de la integral de entropía de Dudley para procesos sub-gaussianos, y una aplicación a la regresión de mínimos cuadrados (dispersa) con una tasa óptima. El proyecto se llevó a cabo utilizando un flujo de trabajo colaborativo humano-IA, en el que los humanos diseñan las estrategias de demostración y los agentes de IA ejecutan la construcción táctica de las pruebas, dando como resultado una caja de herramientas para SLT en Lean 4 verificada por humanos. Más allá de la implementación, el proceso de formalización expone y resuelve supuestos implícitos y detalles faltantes en los libros de texto estándar de SLT, imponiendo una comprensión granular, línea por línea, de la teoría. Este trabajo establece una base formal reutilizable y abre la puerta a desarrollos futuros en la teoría del aprendizaje automático. El código está disponible en 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