Formalizing statistical learning theory in Lean 4 [R]

I’ve been working on a Lean 4 project focused on formalizing parts of statistical learning theory: FormalSLT repository Current 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 main idea is to build a readable and pedagogically structured “theorem ladder” for ML theory rather than just isolated declarations.