Building a readable Lean 4 theorem ladder for statistical learning theory

I’ve been building a Lean 4 project focused on formalizing parts of statistical learning theory:

FormalSLT repository

Current verified results include:

• finite-class ERM bounds
• Rademacher symmetrization
• high-probability Rademacher bounds
• Sauer–Shelah / VC-dimension bridge
• finite scalar contraction
• linear predictor bounds
• finite PAC-Bayes bounds
• algorithmic stability

The project currently has:

• 45 Lean modules
• ~19.5k lines
• zero sorry
• zero custom axioms

The main goal is not just theorem proving for its own sake, but trying to make statistical learning theory more explicit and auditable:

• assumptions are attached directly to theorem signatures
• constants are machine checked
• proofs become buildable dependency chains instead of only textbook prose

I’m also trying to structure it pedagogically as a “theorem ladder”:
definitions → concentration → Rademacher → VC/PAC → stability → PAC-Bayes.

Compared to some existing Lean learning-theory work that focuses more on abstract probability infrastructure, this repo is currently more focused on readable finite-sample ML bounds and end-to-end theorem chains.

Would especially appreciate feedback from people interested in:

• ML theory
• theorem proving
• formal methods
• learning theory pedagogy