Formal Proofs in Applied Mathematics: A Coq Formalization of Simplicial Lagrange Finite Elements
Monday 9 December 2024 at 14h00
ENS Paris-Saclay, Room 1B26
Abstract. This thesis is dedicated to developing formal proofs of mathematical theorems and propositions within the field of real analysis using the Coq proof assistant to ensure their correctness. The core of this work is divided into two main parts. The first part focuses on using Coq to formalize key mathematical principles such as the Lebesgue induction principle and the Tonelli theorem, allowing the computation of double integrals on product spaces by iteratively integrating with respect to each variable. This work builds upon previous research in measure theory and the Lebesgue integral. The second part of this thesis operates within the framework of the Finite Element Method (FEM), a widely used numerical technique for solving partial differential equations (PDEs). FEM plays an important role in numerous industrial simulation programs, particularly in approximating solutions to complex problems such as heat transfer, fluid dynamics, and electromagnetic field simulations. Specifically, we aim to construct finite elements, focusing on simplicial Lagrange finite elements with evenly distributed degrees of freedom. This work engages a broad range of algebraic concepts, including finite families, monoids, vector spaces, affine spaces, substructures, and finite-dimensional spaces. To conduct this study, we formalize in Coq in classical logic several foundational components. We begin by constructing a general finite element, then proceed to define several foundational components, including the construction of the Lagrange approximation space, expressing its Lagrange polynomial basis, and formalizing affine geometric transformations and the unisolvence property of Lagrange finite elements.
Thesis supervisors: Sylvie Boldo, François Clément, and Micaela Mayero
Jury:
- Sylvain Conchon, Université Paris-Saclay – Examinateur
- Laura Grigori, EPFL – Examinatrice
- Sébastien Impériale, Inria – Examinateur
- Damien Pous, CNRS and ENS Lyon – Rapporteur
- Alan Schmitt, Inria – Rapporteur