About statlib
statlib exists to fill a foundation gap. Many statistical and machine-learning arguments need basic formalized material that is missing, scattered, or awkward to use. statlib provides that lower-level infrastructure — and a growing set of usable formal results — on top of Mathlib, so future formalization has something to build on.
Architecture
The library is organized by statistical and machine-learning domains — you find material by mathematical topic, not by the source a theorem came from. Inside each area, the structure has two complementary parts:
Concepts & structures
Names for the objects, assumptions, predicates, models, classes, and reusable vocabulary specific to that area — easy to import and reuse.
Results & proofs
Theorems, lemmas, properties, and proof infrastructure for the main subclasses and standard results in that area.
- Prefer reusable definitions and theorem statements over one-off encodings.
- Keep topic boundaries clear enough that users can import only what they need.
- Choose representative results that clarify the structure of a field.
- Avoid long proof developments whose final statements are hard to apply elsewhere.
- When adding specialized results, expose the assumptions, intermediate lemmas, and vocabulary that make them reusable.
Current status
lake build Statlib
builds the main imported library. The source tree contains 470 Lean
files and 452,823 lines, including 1,807
theorem declarations and 1,035 supporting lemmas.
The core tree has zero sorry placeholders.
New foundation layers include stochastic-order
asymptotics (big-O/little-o in probability, Slutsky),
uniform integrability,
conformal prediction,
low-rank matrix recovery, and
dimension-free Gaussian Lipschitz concentration.
The library depends on Mathlib only.
Roadmap
Today the work centers on three modules; each has its own near-term direction:
Statistical foundations
Statlib.StatFoundation Grow shared vocabulary as concepts get reused across areas, broaden the estimation, testing, empirical-process, and asymptotic foundations, and expand stochastic-order and conformal-inference toolchains.
High-dimensional statistics
Statlib.HighDim Strengthen the operator-convexity, matrix-concentration, covariance, RIP, spectral-perturbation, debiasing, and regression theorem chains; extend L1-process results to broader design matrix families.
Nonparametric statistics
Statlib.Nonparametric Fill in the remaining nonparametric approximation chains while keeping the sieve and risk interfaces reusable across estimators; extend conformal-prediction results to broader nonparametric settings.
Across the library
- Extend the Gaussian functional-inequality, stochastic-order, and nonparametric approximation developments.
- Extend conformal-prediction and uniform-integrability results into reusable toolchains.
- Keep proof narratives and architecture diagrams useful as the dependency graph grows.
Recent growth has added stochastic-order asymptotics with Slutsky-type
product theorems, uniform-integrability and integral-convergence
infrastructure, conformal-prediction foundations, L1-process analysis,
empirical-process results, high-dimensional anisotropic concentration,
operator-convex matrix analysis, and nonparametric sieve approximation.
Recent nonparametric additions include high-order multivariate B-spline
approximation and Holder-smooth ReLU-network rates with the
-2s/d exponent.