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 / …