Formalization of mathematical results in Lean

In this repository, we formalize some mathematical results using Lean 4 and Mathlib.

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

Usage

To use the formalizations, you need to install Lean. Clone the repository, go in any of subdirectory and run lake exe cache get to get the dependencies. Then, you can run lake build to build the project. The generation of the html files uses Alectryon and LeanInk.