Statistische Lerntheorie in Lean 4: Empirische Prozesse von Grund auf

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

Wir präsentieren die erste umfassende Lean-4-Formalisierung der statistischen Lerntheorie (SLT), die in der Theorie empirischer Prozesse verankert ist. Unsere durchgängige formale Infrastruktur implementiert die fehlenden Inhalte in der neuesten Lean-4-Mathlib-Bibliothek, einschließlich einer vollständigen Entwicklung der Gaußschen Lipschitz-Konzentration, der ersten Formalisierung des Dudley'schen Entropie-Integraltheorems für sub-Gaußsche Prozesse und einer Anwendung auf (sparse) Kleinste-Quadrate-Regression mit einer scharfen Konvergenzrate. Das Projekt wurde mittels eines menschlich-KI-kollaborativen Arbeitsablaufs durchgeführt, bei dem Menschen Beweisstrategien entwerfen und KI-Agenten die taktische Beweiskonstruktion ausführen, was zu einem von Menschen verifizierten Lean-4-Werkzeugkasten für SLT führte. Über die Implementierung hinaus deckt der Formalisierungsprozess implizite Annahmen und fehlende Details in Standard-SLT-Lehrbüchern auf und löst diese, was ein detailliertes, zeilenweises Verständnis der Theorie erzwingt. Diese Arbeit schafft eine wiederverwendbare formale Grundlage und ebnet den Weg für zukünftige Entwicklungen in der Maschinellen-Lernen-Theorie. Der Code ist verfügbar unter 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