Статистическая теория обучения в Lean 4: эмпирические процессы с нуля
Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
February 2, 2026
Авторы: Yuanhe Zhang, Jason D. Lee, Fanghui Liu
cs.AI
Аннотация
Мы представляем первую комплексную формализацию теории статистического обучения (ТСО) в Lean 4, основанную на теории эмпирических процессов. Наша сквозная формальная инфраструктура реализует недостающий контент для последней версии библиотеки Lean 4 Mathlib, включая полную разработку гауссовской липшицевой концентрации, первую формализацию теоремы об энтропийном интеграле Дадли для субгауссовских процессов и применение к (разреженной) регрессии методом наименьших квадратов с точной скоростью сходимости. Проект был выполнен с использованием совместного человеко-ИИ рабочего процесса, в котором люди разрабатывали стратегии доказательств, а агенты ИИ выполняли тактическое построение доказательств, что привело к созданию проверенного человеком инструментария для ТСО в Lean 4. Помимо реализации, процесс формализации выявляет и разрешает неявные предположения и недостающие детали в стандартных учебниках по ТСО, обеспечивая детальное, построчное понимание теории. Данная работа закладывает переиспользуемый формальный фундамент и открывает путь для будущего развития теории машинного обучения. Код доступен по адресу 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