Robby955/FormalSLT

来源：https://github.com/Robby955/FormalSLT

基于 Lean 4 的形式化统计学习理论

CI (https://github.com/Robby955/lean-statistical-learning/actions/workflows/ci.yml) Lean 4 (https://lean-lang.org/) Mathlib (https://github.com/leanprover-community/mathlib4) 零个 sorry 公理 许可证：MIT

FormalSLT 是一个紧凑的 Lean 4 库，专注于从经验风险最小化到 VC 风格泛化界的有限样本统计学习理论路径，并包含近期在收缩、线性预测器、有限次高斯链、算法稳定性和有限 PAC-Bayes 置信界方面的扩展，以及首个用于 Dudley 途径的全有界有限网桥接。

45 个 Lean 模块。零个 sorry。零个 admit。零个自定义公理。

公开定理主干使用的公理： [propext, Classical.choice, Quot.sound]。

FormalSLT 定理链

核心路径从 ERM 出发，依次经过 Rademacher 对称化、高概率 Rademacher 界、Massart 界、Sauer-Shelah 界、二元 VC 桥接、有限收缩、线性预测器、有限次高斯链、有限 Dudley 熵预算包装器、有限算法稳定性、有限局部化 Rademacher 脚手架、有限 PAC-Bayes KL/DV/MGF 与有界损失置信界，以及用于后续 Dudley 步骤的全有界有限网适配器。

从何处开始

• 面向机器学习读者： 从如何阅读证明开始，然后阅读直觉。
• 面向证明结构： 请查看图表。
• 面向精确定理名称： 请使用定理映射。
• 面向范围和假设： 阅读假设与当前边界。
• 面向贡献者： 阅读贡献指南，然后阅读好的入门问题。
• 面向相关的 Lean 项目： 请查看相关工作。在该领域还有其他 Lean 形式化工作，例如 YuanheZ/lean-stat-learning-theory (https://github.com/YuanheZ/lean-stat-learning-theory)。该项目采用了不同的方法，开发了经验过程基础设施；而 FormalSLT 直接针对有限样本 PAC、Rademacher 和稳定性界。

为何重要

统计学习理论有许多优美的论文证明，但其假设在文字描述中容易模糊。FormalSLT 将一条可读的有限样本路径转化为机器检查的 Lean 陈述，使得每个界限都在定理签名中携带其假设、常数和有限类作用域。其动机包括：

• 可重现性。 每一个常数——8B2 指数、2 * E[Rad] 因子、(en/d)^d Sauer-Shelah 闭式——都是 Lean 项，内核在每次构建时都会重新检查。不存在隐式的“不失一般性”或“至多常数因子”。
• 教学课程。 阅读 README 的研究生可以点击跳转到他们在黑板上见过的任何界限的精确 Lean 陈述，并且假设在类型签名中明确给出。
• 前沿机器学习。 随着学习理论越来越多地反馈到现代深度学习分析中（PAC-Bayes 泛化、稳定性、链），拥有一个经检查的有限脚手架是迈向对这些方法本身进行形式化保证的第一步。

定理系列

范围与假设

主要的泛化定理特意设计为有限且显式。

当前边界

简短版本：

• 主要的 Rademacher 和 VC 结果是有限类/有限样本定理。
• 高概率 Rademacher 界使用 Azuma 8B² 指数；更锐利的 McDiarmid 常数留待未来工作。
• 链层证明了有限熵预算基础设施和首个全有界有限网提取桥接，而非连续 Dudley 积分。
• PAC-Bayes 包含一个有界 [0,1] 损失 Catoni 风格置信界、一个闭式高置信好事件定理、一个固定预算 McAllester 风格平方根推论、以及一个用于后验相关惩罚的有限网格剥离包装器。精确的全实 λ、无限假设和连续后验变体留待未来工作。
• 算法稳定性包含有限独立同分布和测度论独立同分布期望间隙包装器，以及针对有限可测假设接口的有界损失高概率包装器。

完整范围声明请参见假设与当前边界。

安装

本项目需要 elan (https://github.com/leanprover/elan)，即 Lean 工具链管理器。elan 将读取 lean-toolchain 并自动获取固定的 Lean 版本。

git clone https://github.com/Robby955/lean-statistical-learning.git
cd lean-statistical-learning
lake exe cache get      # 下载预编译的 Mathlib oleans
lake build FormalSLT    # 构建库

如果 lake 不在 shell 路径中，请直接使用 elan 二进制文件：

~/.elan/bin/lake exe cache get
~/.elan/bin/lake build FormalSLT

首次构建需要几分钟（下载 Mathlib 缓存）；之后构建将是增量式的。

发布候选检查

在将分支视为展示候选之前，请运行以下命令：

lake exe cache get
lake build FormalSLT
lake env lean examples/CheckShowcaseTheorems.lean

审计命令

使用上述发布候选检查，然后运行证明债务和空白审计：

rg -n --pcre2 '^\s*(?:by\s+)?(?:sorry|admit)\b|:=\s*(?:by\s+)?(?:sorry|admit)\b' FormalSLT examples
rg -n --pcre2 '^\s*(?:axiom|constant)\s+[A-Za-z_]' FormalSLT examples
git diff --check

预期结果如下：

• lake build FormalSLT 成功退出；
• examples/CheckShowcaseTheorems.lean 打印所选公开定理的标准 Lean/Mathlib 公理；
• rg 命令在 FormalSLT 或 examples 中未发现任何可执行的 sorry、可执行的 admit 以及自定义公理/常量；
• git diff --check 未报告空白错误。

模块映射

路线图

• 有限样本 Rademacher 定义
• Rademacher 对称化
• Massart 有限类界
• Azuma-Hoeffding 泛化间隙尾部
• 高概率 Rademacher 界
• Sauer-Shelah 多项式界
• VC 风格逐点 Rademacher
• VC 一致偏差与 ERM 过剩风险尾部
• VC 闭式 ERM 样本复杂度定理
• 二元类 VC 到有效损失模式桥接
• 有限样本标量收缩
• 有限维线性预测器 Rademacher 界
• 有限局部化 Rademacher/Bernstein 方差局部化脚手架
• 覆盖数剥离与两尺度链
• 有限次高斯最大与有限链熵预算
• 算法稳定性有界差分脚手架
• 有限算法稳定性在坐标交换恒等式下的期望间隙适配器
• 有限独立同分布坐标交换恒等式与字面期望泛化间隙特化
• 有限独立同分布双侧算法稳定性期望间隙包装器
• PAC-Bayes KL 散度与 Donsker-Varadhan 变分不等式
• PAC-Bayes 有限独立同分布乘积 MGF 桥接用于经验风险偏差
• PAC-Bayes 有界损失 MGF、Markov 置信与有限 Catoni 风格界
• PAC-Bayes 闭式高置信泛化收益定理
• PAC-Bayes 固定预算 McAllester 风格平方根推论
• PAC-Bayes 有限网格 McAllester 剥离与优化的有限网格包装器
• 有限 Dudley 离散熵界精化：环、积分预算与前缀包络包装器
• 全有界有限网提取桥接用于连续 Dudley 途径
• 投影上确界全有界二进 Dudley 包装器
• 投影有限网全有界二进 Dudley 包装器（无需有限环境指标类型）
• 有限二进预算到熵在半径处的上求和比较
• 移位有限环熵预算折叠为一个截断区间积分
• 上确界供给边界适配器，带有显式终端逼近误差
• 有限骨架/稠密网边界适配器，带有显式可分离性与终端投影误差
• 逐路模量与有限骨架证言引理，用于满足连续边界适配器的假设
• ε化有限选择边界适配器：每个正误差预算均可由有限骨架与终端二进尺度证书处理
• 有限覆盖/逐路模量证书用于 ε化全有界 Dudley 边界层
• 有限终端全有界二进 Dudley 包装器
• 全有界类上的连续 Dudley 熵积分定理
• 测度论独立同分布算法稳定性期望界，带有显式可积性假设
• 有界损失可测性适配器用于测度论稳定性期望间隙定理
• 有界损失高概率稳定性包装器用于有限可测假设接口
• PAC-Bayes 全实 λ 或连续后验扩展
• 锐利 McDiarmid/乘积核分解
• 连续 Dudley 风格熵积分

依赖

• Lean 4 (https://lean-lang.org/) v4.30.0-rc2
• Mathlib4 (https://github.com/leanprover-community/mathlib4) @ 25b7ac7

贡献

欢迎贡献。请在打开拉取请求前阅读 CONTRIBUTING.md。简短版本：每个拉取请求一个定理，无 sorry/无 admit，仅使用标准 [propext, Classical.choice, Quot.sound] 公理，假设在类型签名中声明而非埋在假设中。

关于想法，请查看开放形式化问题列表、好的入门问题以及上面路线图中未勾选的项。公开发布前，维护者可以使用公开发布检查清单。

引用

如果您在学术工作中使用 FormalSLT，请引用：

@software{formal_slt,
  title  = {FormalSLT: Formal Statistical Learning Theory in Lean 4},
  author = {Sneiderman, Robby},
  year   = {2026},
  url    = {https://github.com/Robby955/lean-statistical-learning},
  note   = {Lean 4 formalization of finite-sample SLT bounds.}
}

许可证

本项目采用 MIT 许可证发布。