This repository collects efforts to formalize results on machine learning following the book "Understanding Machine Learning" by Shalev-Shwartz and Ben-David.
It features the following verifications:
- Basics:
LearningTheory
formalizes basic notation from Chapter 2FiniteHypClasses
proves that finite Hypothesis classes are PAC
- VC dimension:
VCDim
formalizes results from Chapter 6
- Boosting:
Boosting
formalizes AdaBoost following Chapter 10
- Soft SVM:
SVM
formalizes soft SVM following Chapter 15