Teoria da Aprendizagem Estatística no Lean 4: Processos Empíricos do Zero
Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
February 2, 2026
Autores: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
cs.AI
Resumo
Apresentamos a primeira formalização abrangente em Lean 4 da teoria da aprendizagem estatística (SLT) fundamentada na teoria dos processos empíricos. Nossa infraestrutura formal de ponta a ponta implementa os conteúdos ausentes na biblioteca mais recente do Lean 4 Mathlib, incluindo um desenvolvimento completo da concentração gaussiana lipschitziana, a primeira formalização do teorema da integral de entropia de Dudley para processos sub-gaussianos e uma aplicação à regressão por mínimos quadrados (esparsa) com uma taxa ótima. O projeto foi realizado usando um fluxo de trabalho colaborativo humano-IA, no qual humanos projetam estratégias de prova e agentes de IA executam a construção tática de provas, resultando na caixa de ferramentas para SLT em Lean 4 verificada por humanos. Além da implementação, o processo de formalização expõe e resolve pressupostos implícitos e detalhes ausentes nos livros didáticos padrão de SLT, impondo uma compreensão granular, linha por linha, da teoria. Este trabalho estabelece uma base formal reutilizável e abre as portas para desenvolvimentos futuros na teoria da aprendizagem de máquina. O código está disponível em 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