Teoria dell'Apprendimento Statistico in Lean 4: Processi Empirici da Zero
Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
February 2, 2026
Autori: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
cs.AI
Abstract
Presentiamo la prima formalizzazione completa in Lean 4 della teoria dell'apprendimento statistico (SLT) basata sulla teoria dei processi empirici. La nostra infrastruttura formale end-to-end implementa i contenuti mancanti nell'ultima libreria Lean 4 Mathlib, includendo uno sviluppo completo della concentrazione Gaussiana-Lipschitz, la prima formalizzazione del teorema dell'integrale di entropia di Dudley per processi sub-gaussiani e un'applicazione alla regressione ai minimi quadrati (sparsa) con un tasso ottimale. Il progetto è stato realizzato utilizzando un flusso di lavoro collaborativo uomo-IA, in cui gli esseri umani progettano le strategie di dimostrazione e gli agenti di IA eseguono la costruzione tattica delle prove, portando alla creazione di una toolbox verificata da umani in Lean 4 per la SLT. Oltre all'implementazione, il processo di formalizzazione espone e risolve assunzioni implicite e dettagli mancanti nei manuali standard di SLT, imponendo una comprensione granulare, riga per riga, della teoria. Questo lavoro stabilisce una base formale riutilizzabile e apre la porta a futuri sviluppi nella teoria dell'apprendimento automatico. Il codice è disponibile all'indirizzo 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