## Formalization of Mathematics

In order to formally prove the corresponding programs, we need (applied) mathematics to be formalized too. Therefore, I have been involved in several libraries of formalized mathematics.

The **coq-num-analysis** library (also an opam package)
includes many results of numerical analysis, including the Lebesgue
integration of nonnegative functions and the Lax-Milgram
theorem.

François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine, and I are currently working on the formalization of the Finite Elements Methods.

With François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis, we formally proved correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors.

We developed the Coquelicot library about real analysis with Guillaume Melquiond and Catherine Lelay.