Statistische Leertheorie in Lean 4: Empirische Processen vanaf de Basis

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

February 2, 2026

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

cs.AI

Samenvatting

Wij presenteren de eerste uitgebreide Lean 4-formalisering van de statistische leertheorie (SLT), gegrondvest in de theorie van empirische processen. Onze end-to-end formele infrastructuur implementeert de ontbrekende inhoud in de nieuwste Lean 4 Mathlib-bibliotheek, inclusief een complete ontwikkeling van Gaussische Lipschitz-concentratie, de eerste formalisering van Dudley's entropie-integraalstelling voor sub-Gaussische processen, en een toepassing op kleinste-kwadraten-(schaarse)regressie met een scherpe snelheid. Het project werd uitgevoerd met behulp van een mens-AI-samenwerkingsworkflow, waarbij mensen bewijsstrategieën ontwerpen en AI-agenten tactische bewijsconstructie uitvoeren, wat leidde tot de door mensen geverifieerde Lean 4-toolbox voor SLT. Naast de implementatie legt het formaliseringsproces impliciete aannames en ontbrekende details in standaard SLT-leerboeken bloot en lost deze op, waardoor een gedetailleerd, regel-voor-regel begrip van de theorie wordt afgedwongen. Dit werk vestigt een herbruikbare formele basis en opent de deur voor toekomstige ontwikkelingen in de machinaal leren-theorie. De code is beschikbaar op 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