Robby955formal-slt

Machine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.

FormalSLT

CI Docs Release Lean 4 Mathlib License: MIT

FormalSLT is a Lean 4 library for statistical learning theory and modern finite-sample inference.

It develops reusable results in VC and Rademacher theory, metric entropy and chaining, PAC-Bayes bounds, confidence sequences and e-processes, and learning from adaptive or dependent trajectories. The goal is a coherent Lean foundation in which classical learning theory and newer sequential methods can be composed and extended.

Worked applications show how these parts of the library combine.

Documentation · Theorem map · Search declarations · Install

Overview video

FormalSLT overview film

Fixed-time guarantees can fail under repeated monitoring; one checked event can cover repeated looks. The repo-wide film starts there, then maps reusable proof infrastructure across VC and Rademacher theory, chaining, PAC-Bayes, e-processes, and dependent-data inference. It establishes the platform and its current interfaces; it does not claim end-to-end verification of an ML system.

Play the responsive film · Transcript · Manim source · Pinned v0.2.0 film receipt

Results

Classical learning theory

FormalSLT includes Sauer-Shelah bounds for finite set families, VC-based uniform-deviation and ERM excess-risk bounds for binary zero-one loss, finite-sample Rademacher symmetrization, Massart bounds, contraction, linear-predictor bounds, and metric-entropy estimates. Its chaining results reach total-bounded spaces and continuous entropy-integral bounds while keeping the required boundary, separability, and modulus assumptions explicit.

VC source · Rademacher source · chaining source · theorem map

Anytime PAC-Bayes and empirical Bernstein

For an infinite IID sequence, one event controls every sample size n ≥ 2 and every admissible posterior. The bound uses Bessel sample variance and measure-theoretic KL divergence. A separate forward construction handles predictable residuals for sequential use. The all-sample result is uniform over sample size, but it is not an optional-stopping theorem.

Lean source · checker · positive-KL example

Adaptive trajectories

For a finite score family fixed in advance, one event allows the posterior and tilt to depend on the observed prefix and time. With the geometric time selector, the resulting width tends to zero. A separate theorem covers measurable state and hypothesis spaces with a finite tilt family. These results start from a deterministic initial state and bound prefix-conditional risk.

finite-state source · measurable-space source · worked checker

Stationary and Markov risk

Prequential bounds combine with finite-depth Poisson corrections to control stationary risk. One route uses a known contracting kernel. The empirical route uses a finite catalog of contracting candidates and requires every source row to be visited. A selected empirical contraction bound below one additionally proves uniqueness of the true invariant law.

known-kernel source · candidate-family source · worked checker

Controlled queue

For a 24-state controlled queue, the generic transition bound allocates confidence across 48 × 48 × 2 = 4,608 coordinates. Under a specified one-parameter refresh model, a single destination-hit statistic has a row-independent conditional mean, and Lean proves that its parameter discrepancy equals physical-row total variation. This example is retrospective and conditional on the refresh model; it does not test family membership.

application · design · Lean receipt

Install

FormalSLT currently uses Lean 4.32.2 and Mathlib 4.32.2. The stable topic imports are:

import FormalSLT.PACBayes
import FormalSLT.Sequential
import FormalSLT.StochasticDynamics
import FormalSLT.VC

Add the latest tagged release to a Lake project:

require «formal-slt» from git
  "https://github.com/Robby955/FormalSLT.git" @ "v0.2.0"

For unreleased work, pin a full commit SHA that you have reviewed rather than the moving branch.

Then run:

lake update
lake exe cache get
lake build

v0.2.0 release notes

Repository layout

  • FormalSLT/PACBayes: PAC-Bayes inequalities and change-of-measure tools
  • FormalSLT/Rademacher: symmetrization, contraction, and generalization bounds
  • FormalSLT/Covering: metric entropy and chaining
  • FormalSLT/Sequential: confidence sequences, e-processes, and Ville bounds
  • FormalSLT/StochasticDynamics: adaptive paths, kernels, and stationary risk
  • FormalSLT/VC: VC dimension, growth functions, and uniform convergence
  • examples: small checker files for public results
  • applications: end-to-end worked examples

Verify

lake exe cache get
lake build FormalSLT
make examples
make tutorials
make api
make downstream

Verification details

Papers and references

Contributing

See CONTRIBUTING.md and the good first issues.

License

MIT. See LICENSE.