- Formalization of some results of the book
*Éléments d'Analyse Fonctionnelle*by Francis Hirsch and Gilles Lacombe. - Formalization of the representation of finite groups as Cayley's graphs.
- Formalization of the measure representation of ultrafilters.
- Formalization of the total law of expectation/probability.