用形式化方法在Lean 4中完整实现统计学习理论，提升理论严谨性。
AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory
- 通过人机协作在Lean 4中构建统计学习理论的形式化框架。
- 实现高斯Lipschitz集中与Dudley熵积分定理，给出稀疏回归的精确率。
- 揭示教科书中的隐藏假设，适合形式化验证和机器学习理论研究者。
我们首次在Lean 4中完成了基于经验过程理论的统计学习理论（SLT）完整形式化。该端到端形式化基础设施填补了最新Lean库的空白，包含高斯Lipschitz集中、子高斯过程的Dudley熵积分定理，以及最小二乘（稀疏）回归的精确率分析。项目采用人机协同工作流，人类设计证明策略，AI代理执行战术构造，最终生成经人工验证的可复用的Lean 4 SLT工具箱。形式化过程暴露并修正了标准教材中的隐含假设与缺失细节，推动对理论进行逐行精细理解。本工作建立可复用的形式化基础，为未来机器学习理论发展开辟路径。代码见：https://github.com/YuanheZ/lean-stat-learning-theory。
原文摘要 · Abstract (English)
We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our en-to-end formal infrastructure implement the missing contents in latest Lean library, including a complete development of Gaussian Lipschitz concentration, 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 provided in https://github.com/YuanheZ/lean-stat-learning-theory.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。