← 返回总览

ML Lib (MLMath) · 库统计

Lean 4 + Mathlib 的机器学习理论库 · ML_lib/lean_project/MLMath · 已忽略 Bridge/ 与 SmokeTests.lean

911

声明总数

641

定理 + 引理

214

定义 def+abbrev

19.3K

代码行

要点

完全证完:911 个声明无任何 sorry / admit,0 自定义 axiom,全部基于 Mathlib。
73 个 .lean 文件、9 个顶层模块;另有 DEFS_INDEX.md 索引 250 个定义级 API。
过重、当前 Mathlib 不便完成的辅助命题:整条不收录(注释标 NO sorry),不留占位。

按模块(声明数)

Statistics240

MLSetup217

Optimization144

Probability120

Calculus104

Measure37

LinearAlgebra20

InformationTheory17

Analysis12

模块明细

模块	定理	引理	def	其他*	合计	LOC	内容
Statistics	16	156	53	15	240	6345	Rademacher / covering / VC
MLSetup	1	116	74	26	217	2357	risk/loss/sample、算法
Optimization	74	27	34	9	144	4291	凸/强凸、GD、在线、非凸
Probability	42	54	16	8	120	3662	集中不等式、鞅、bandit
Calculus	87	11	6	0	104	1293	次微分、梯度/Hessian
Measure	5	22	6	4	37	571	轨迹测度、核
LinearAlgebra	1	12	0	7	20	387	PosDef、矩阵 L2、伪逆
InformationTheory	0	10	6	1	17	208	KL 散度、熵
Analysis	2	5	3	2	12	184	Lp 空间
合计	228	413	198	72	911	19329

*其他 = abbrev 16 + structure 15 + class 9 + instance 32。证明性内容(定理+引理)占 70%。

口径:扫描 MLMath/**/*.lean(忽略 Bridge / _jsonl / SmokeTests);sorry/axiom 已用排除注释的精确匹配复核为 0。