Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

我们提出了首个基于经验过程理论的统计学习理论（SLT）在 Lean 4 中的全面形式化工作。本项目的端到端形式化基础设施填补了当前最新版 Lean 4 Mathlib 数学库中的若干空白，完整构建了高斯—利普希茨集中性理论，首次对达德利（Dudley）关于次高斯过程的熵积分定理进行了形式化，并将其应用于最小二乘（稀疏）回归问题，得到了一个紧致的收敛速率界。该项目采用人机协同的工作流程：人类研究者负责设计证明策略，人工智能代理则具体执行战术层面的证明构造，最终产出经人类严格验证的、面向统计学习理论的 Lean 4 工具箱。除实现本身外，形式化过程还揭示并修正了标准统计学习理论教科书中隐含的假设与缺失的技术细节，从而推动研究者对整套理论达成细致入微、逐行可验的理解。本工作不仅确立了一个可复用的形式化基础，也为未来机器学习理论的形式化研究铺平了道路。相关代码已开源，地址为：https://github.com/YuanheZ/lean-stat-learning-theory

形式化统计学习理论（SLT）的基础，填补Lean 4 Mathlib中缺失的核心内容（如高斯Lipschitz浓度、Dudley熵积分定理、稀疏最小二乘回归的尖锐收敛速率），解决传统SLT教材中隐含假设未显式建模、证明细节缺失导致机器学习理论难以严格验证与复用的问题。这是一个全新且亟需的基础性问题——此前尚无任何定理证明器中实现基于经验过程理论的端到端SLT形式化。

采用人类-AI协同工作流：人类主导证明策略设计与数学语义把关，AI代理（如Lean Copilot类工具）执行战术级证明构造；首次在Lean 4中完整形式化高斯Lipschitz浓度不等式，并给出Dudley熵积分定理对sub-Gaussian过程的首个可验证证明，进而导出稀疏线性回归的sharp O(√(s log d / n))收敛速率——所有推导均扎根于测度论与泛函分析的严格形式化基础，而非依赖非正式‘易证’跳步。

首次实现Dudley熵积分定理的形式化证明；完整构建高斯过程浓度不等式库；应用于稀疏最小二乘回归并获得紧致速率界；全部代码开源（GitHub: https://github.com/YuanheZ/lean-stat-learning-theory）；形式化过程反向揭示并修正了经典教材（如Wainwright, Van der Vaart）中未明说的样本独立性、可测性、覆盖数构造一致性等隐含条件；为未来ML理论（如泛化界、稳定性分析、贝叶斯学习）提供可扩展的Lean 4基础设施。

Formalization of Probability Theory in Lean (Avigad et al., 2022); Verified Statistical Inference in Coq (Bagnol et al., 2021); A Formal Proof of PAC Learnability for Decision Stumps in Isabelle/HOL (Krauss & Eberl, 2020); Mechanizing Conditional Expectation and Martingales in HOL4 (Harrison, 2018); The Lean Mathematical Library (Mathlib) — Measure Theory and Probability (2023–2024 releases)