StatsMLlib: A Lean 4 Library Formally Verifying Probability, Statistics, and ML Theorems
ChengleiSi · x · 2026-08-03
StatsMLlib is a formal mathematics library in Lean 4, aiming to provide a unified foundation for probability, statistics, and machine learning. It covers concentration inequalities, metric entropy and chaining, empirical processes, Rademacher complexity, random matrix theory, and finite-sample learning guarantees, with every proof checked by the Lean 4 kernel. The library currently includes 666 theorems, 1,219 lemmas, 352 definitions, 89 Lean files, and 64,695 lines of Lean code, with zero sorries. Organized by Fanghui Liu and Jason D. Lee, contributions are welcome.
More from Research
- AI generates too many hypotheses, lab capacity becomes the new science bottleneck — VraserX · 2026-08-03
- Researchers Slam NeurIPS Review Process: Ghosting and Lack of Accountability — RexDouglass · 2026-08-03
- HorizonMath Benchmark Released: GPT-5.4 Pro Discovers Novel Math Solutions — RexDouglass · 2026-08-03
- NeurIPS Peer Review is Broken: Exponential Submissions Meet LLM-Generated Reviews — RexDouglass · 2026-08-03
- LLM Safety Trilemma: Useful Capability, Reliable Safety, and Open Access Cannot Coexist — Pingyu Wu · 2026-08-03
- Replicating the Test: Can LLMs Spell Words Based on Audio? — theshawwn · 2026-08-03