Lean 4 中的统计学习理论：从零开始的经验过程
机器学习
2026-02-03 v1 计算与语言
统计理论
统计理论
摘要
我们提出了首个基于经验过程理论的完整Lean 4形式化统计学习理论（SLT）。我们的端到端形式化基础设施实现了最新Lean 4 Mathlib库中缺失的 contents，包括高斯 Lipschitz 集中不等式的完整发展、亚高斯过程 Dudley 熵积分定理的首个形式化，以及针对最小二乘（稀疏）回归的应用（带尖锐收敛率）。该项目采用人类-AI协作工作流程实现，人类设计证明策略，AI代理执行战术证明构建，最终形成经人验证的Lean 4SLT工具箱。除实现外，形式化过程还暴露并解决了标准SLT教科书中潜在假设和遗漏细节，强制进行逐行、细粒度的理论理解。本工作建立了可复用的形式化基础，为机器学习理论的未来发展开辟了道路。代码已发布于 https://github.com/YuanheZ/lean-stat-learning-theory
关键词
引用
@article{arxiv.2602.02285,
title = {Statistical Learning Theory in Lean 4: Empirical Processes from Scratch},
author = {Yuanhe Zhang and Jason D. Lee and Fanghui Liu},
journal= {arXiv preprint arXiv:2602.02285},
year = {2026}
}
备注
19 pages, 2 figures. Comments are welcome