Lean 4 新库 StatsMLlib：形式化验证概率统计与机器学习定理

ChengleiSi · x · 2026-08-03

StatsMLlib 是一个基于 Lean 4 的形式化数学库，旨在为概率、统计和机器学习提供统一的形式化基础。该库涵盖了集中不等式、度量熵与链式法则、经验过程、Rademacher 复杂度、随机矩阵理论以及有限样本学习保证等主题，所有证明均由 Lean 4 内核验证。目前包含 666 个定理、1219 个引理、352 个定义、89 个 Lean 文件，共 64,695 行代码，且无未完成的证明（0 sorries）。项目由 Fanghui Liu 和 Jason D. Lee 组织，欢迎社区贡献。