Thèse préparée au sein du Laboratoire Méthodes Formelles (Université Paris-Saclay, CNRS, ENS Paris-Saclay), sous la direction de Sylvie Boldo, directrice de recherche, la co-direction de Micaela Mayero, maîtresse de conférences, et le co-encadrement de François Clément, chargé de recherche.
La thèse a été soutenue à Université Paris-Saclay au Laboratoire des Méthodes Formelles (LMF) le 9 décembre 2024 par:
                                                                Houda MOUHCINE
devant un jury composé de:
ـ Sylvain Conchon, professeur des universités à l’Université Paris-Saclay : Président
ـ Damien Pous, directeur de recherche au CNRS et à l’ENS Lyon : Rapporteur et Examinateur
ـ Alan Schmitt, directeur de recherche à l’Inria Rennes : Rapporteur et Examinateur
ـ Laura Grigori, professeure à l’EPFL en Suisse : Examinatrice
ـ Sébastien Impériale, chargé de recherche à l’Inria Saclay : Examinateur
Le problème qui a tout motivé
Imaginez un ingénieur qui conçoit un pont, un médecin qui programme un appareil de radiothérapie, ou un constructeur automobile qui simule les freins d’une voiture autonome. Dans tous ces cas, des logiciels très complexes réalisent des milliers de calculs mathématiques pour prédire ce qui va se passer dans le monde réel. Ces simulations sont censées garantir que le pont tient debout, que la dose de radiation est correcte, que la voiture s’arrête à temps.
Mais voilà le problème fondamental : ces logiciels sont écrits par des humains, et les humains font des erreurs. Une petite coquille dans le code, une hypothèse oubliée dans une formule mathématique, et les résultats peuvent être faux, parfois imperceptiblement, parfois de manière catastrophique. L’histoire de l’informatique en est jalonnée : la sonde Ariane 5 qui explose à cause d’un dépassement de nombre, le logiciel médical Therac-25 qui a irradié mortellement des patients…
La grande question que se pose ma thèse est donc : comment s’assurer, de manière absolument certaine et vérifiable par un ordinateur, que les mathématiques sur lesquelles reposent ces logiciels sont correctes ?
La réponse : les preuves formelles
Dans les mathématiques classiques, un chercheur démontre un théorème sur papier. Il raisonne, argumente, convainc ses collègues. Mais des erreurs peuvent se glisser dans le raisonnement, et parfois elles ne sont découvertes que des années plus tard.
Les preuves formelles, c’est une approche radicalement différente : on confie à un logiciel spécialisé, appelé assistant de preuve, la tâche de vérifier chaque étape du raisonnement, une par une, avec une rigueur absolue. Ce logiciel, qui s’appelle Coq, est incapable d’accepter un argument flou ou une étape manquante. Soit la preuve est parfaite et complète, soit le logiciel refuse. C’est comme si chaque brique d’un mur était vérifiée individuellement avant d’être posée.
Ma thèse consiste précisément à traduire des théorèmes mathématiques complexes dans ce langage de vérification automatique, pour qu’ils soient garantis corrects à 100 %, sans aucune ambiguïté possible.
L’objectif final : certifier les grands logiciels de simulation
L’objectif à long terme, qui est un chantier collectif de plusieurs années, est de vérifier formellement les grands logiciels de simulation scientifique comme FreeFEM++ ou XLiFE++. Ces logiciels sont utilisés dans des industries critiques, aérospatial, nucléaire, médical, génie civil, pour simuler des phénomènes physiques complexes. Leur certifier une correction mathématique absolue représente un enjeu majeur pour la sécurité mondiale.
Mais avant d’arriver là, il faut bâtir les fondations, pièce par pièce. C’est exactement le rôle que joue ma thèse dans ce programme de recherche. Mon travail s’inscrit dans une chaîne de contributions qui a commencé en 2001 avec une bibliothèque formelle pour les nombres réels, puis s’est enrichie au fil des années avec la formalisation de l’intégrale de Lebesgue, du théorème de Lax-Milgram, et d’une première simulation d’équation d’onde. Je prends le relais pour passer à l’étape suivante : la méthode des éléments finis.
Ce que j’ai construit : deux contributions majeures
Première partie :Poser les bases du calcul intégral pour les équations physiques
Pour résoudre des équations physiques complexes, celles qui décrivent la chaleur, les fluides, les vibrations, les champs électromagnétiques, les mathématiciens travaillent avec des objets appelés équations aux dérivées partielles. Ces équations font intervenir des fonctions à plusieurs variables, et pour les manipuler correctement, il faut savoir calculer des intégrales à plusieurs dimensions.
Or, calculer une intégrale à deux variables directement est souvent très difficile. Il existe heureusement un résultat fondamental, le théorème de Tonelli, qui permet de simplifier radicalement ce calcul : plutôt que de tout traiter ensemble, on peut intégrer d’abord par rapport à la première variable, puis par rapport à la seconde, comme si on découpait un rectangle en colonnes une par une. Ce résultat est omniprésent en physique, en probabilités, en analyse numérique.
Ce théorème est donc une brique essentielle pour qui veut, à terme, formaliser la méthode des éléments finis, car cette méthode repose elle-même sur des calculs d’intégrales multiples pour construire ses équations et vérifier ses solutions. C’est le lien direct entre cette première partie et la suite.
J’ai formalisé et prouvé ce théorème dans Coq, en m’appuyant sur des travaux antérieurs de formalisation de l’intégrale de Lebesgue. Pour y arriver, j’ai d’abord dû prouver un outil intermédiaire clé : le principe d’induction de Lebesgue. C’est une technique de raisonnement qui permet de démontrer des propriétés sur une grande famille de fonctions mathématiques en suivant trois étapes progressives, d’abord les fonctions les plus simples (les fonctions indicatrices), puis les fonctions simples non négatives, et enfin toutes les fonctions mesurables non négatives. Ma contribution originale a été de dériver ce principe à partir d’un type inductif dans Coq, une approche nouvelle dans la littérature. Ce travail a été publié en 2023.
Deuxième partie :Construire les éléments finis de Lagrange dans Coq
C’est la partie centrale et la plus ambitieuse de ma thèse. Pour simuler des phénomènes physiques, les ingénieurs utilisent une méthode très puissante appelée la méthode des éléments finis (MEF). L’idée est élégante : plutôt que de résoudre un problème sur tout un domaine complexe, par exemple, toute la carrosserie d’une voiture ou toute la structure d’un barrage, on découpe ce domaine en milliers de petits morceaux simples, généralement des triangles ou des tétraèdres, et on résout le problème localement sur chaque morceau, puis on assemble le tout. Chaque petit morceau est ce qu’on appelle un élément fini.
Les éléments finis de Lagrange sont la famille la plus utilisée en pratique, car ils sont simples et efficaces. Chaque élément est décrit par trois ingrédients : sa forme géométrique, l’espace de fonctions polynomiales qui sert à approximer la solution à l’intérieur de cet élément, et un ensemble de points stratégiques appelés nœuds qui permettent de relier les éléments entre eux de façon cohérente.
La propriété clé qui rend ces éléments mathématiquement valides est ce qu’on appelle l’unisolvance : étant donné les valeurs aux nœuds, il existe une et une seule fonction polynomiale qui leur correspond. Sans cette propriété, la méthode ne fonctionnerait pas, les solutions seraient indéterminées et le logiciel produirait des résultats incorrects.
Ce que j’ai fait dans ma thèse, c’est de prendre toute cette machinerie mathématique et de la formaliser entièrement dans Coq : définir les formes géométriques (les simplexes, généralisation du triangle à toute dimension), construire l’espace des polynômes à plusieurs variables, définir les nœuds de Lagrange et leurs polynômes associés, prouver les transformations géométriques qui permettent de passer d’un élément de référence à n’importe quel autre élément, et enfin démontrer formellement la propriété d’unisolvance, preuve vérifiée ligne par ligne par Coq. C’est l’aboutissement central de ma thèse.
Pour y parvenir, j’ai dû construire un édifice mathématique énorme : des dizaines de définitions et de preuves formelles couvrant les familles finies, les espaces vectoriels, les espaces affines, les polynômes à plusieurs variables, les fonctions bijectives, les transformations géométriques affines, les coordonnées barycentriques… Tout cela vérifié par l’ordinateur, sans la moindre lacune tolérée.
La première partie de ma thèse, le théorème de Tonelli, n’est pas déconnectée de tout cela. Elle prépare le terrain pour les futures étapes : pour vérifier formellement que la méthode des éléments finis converge bien vers la bonne solution, il faudra manipuler des espaces de Sobolev, qui eux-mêmes reposent sur l’intégrale de Lebesgue et ses propriétés multi-dimensionnelles, dont Tonelli fait partie.
Ce que le monde gagne grâce à ce travail
Dans l’aéronautique et le spatial, les simulations de résistance des structures, de dynamique des fluides autour des ailes ou de comportement thermique des moteurs reposent sur la méthode des éléments finis. Des outils formellement certifiés réduisent le risque de défaillances invisibles dans les calculs qui guident ces ingénieries critiques.
Dans le médical, les simulations de propagation de la chaleur lors d’une radiothérapie, ou les simulations mécaniques sur des implants osseux, peuvent bénéficier de cette certification. Une erreur dans un calcul de simulation médicale peut avoir des conséquences irréversibles sur un patient.
Dans le nucléaire et l’énergie, les simulations de comportement des réacteurs ou des structures soumises à des contraintes extrêmes nécessitent une fiabilité absolue. Le travail de certification formelle que j’amorce est une garantie supplémentaire que ces simulations font bien ce qu’elles prétendent faire.
Pour la communauté scientifique, mon travail constitue une base réutilisable et publiquement disponible. Les preuves Coq que j’ai développées sont accessibles en ligne, et d’autres chercheurs peuvent s’en servir pour aller plus loin : formaliser les espaces de Sobolev, les formules de quadrature, et finalement l’ensemble de la méthode des éléments finis, y compris la certification des logiciels FreeFEM++ et XLiFE++ qui en sont l’implémentation industrielle.
Code Coq disponible sur : https://lipn.univ-paris13.fr/coq-num-analysis

ملخص الاطروحة : البراهين الشكلية في الرياضيات التطبيقية: صياغة شكلية للعناصر المحدودة من نوع لاغرانج المبسَّطة
تتناول هذه الأطروحة مشكلة جوهرية تتمثل في أن البرمجيات المستعملة في محاكاة الأنظمة الحساسة، مثل الجسور والأجهزة الطبية والسيارات الذاتية القيادة، تعتمد على حسابات رياضية معقدة، لكن أي خطأ بسيط في البرمجة أو في الصياغة الرياضية قد يؤدي إلى نتائج خطيرة جدًا. ومن هنا يتركز هدف البحث على إيجاد وسيلة تضمن بشكل يقيني وصارم صحة الأسس الرياضية التي تعتمد عليها هذه البرمجيات. ولتحقيق ذلك، اعتمدت الأطروحة على منهج البرهان الشكلي، وهو أسلوب يقوم على تحويل البراهين الرياضية إلى صيغة دقيقة يمكن لبرنامج حاسوبي متخصص أن يتحقق منها خطوةً خطوةً دون أن يقبل أي غموض أو نقص في الاستدلال.
يندرج هذا العمل ضمن مشروع علمي طويل المدى يهدف إلى التحقق الكامل من صحة برامج المحاكاة العلمية المستعملة في مجالات شديدة الحساسية مثل الطيران والطاقة والطب والهندسة المدنية. وفي هذا الإطار قدمت الأطروحة مساهمتين أساسيتين. تمثلت الأولى في الصياغة الشكلية لمبرهنة أساسية في حساب التكاملات المتعددة، وهي مبرهنة تونيلّي، التي تسمح بتبسيط حساب التكاملات ذات عدة متغيرات عبر تحويلها إلى تكاملات متتالية أسهل في الحساب، وهو أمر ضروري في دراسة المعادلات التي تصف الظواهر الفيزيائية. ولإثبات هذه النتيجة داخل النظام الحاسوبي، تم تطوير أداة برهانية وسيطة تعتمد على بناء تدريجي للخصائص الأساسية للتكامل، انطلاقًا من الدوال البسيطة ثم تعميمها إلى حالات أكثر تعقيدًا، وذلك بطريقة شكلية دقيقة داخل بيئة التحقق الآلي.
أما المساهمة الثانية، وهي جوهر الأطروحة، فقد تمثلت في بناء صياغة شكلية كاملة للعناصر المحدودة من نوع لاغرانج، وهي من أكثر الأدوات استعمالًا في المحاكاة العددية للظواهر الفيزيائية. وتقوم الفكرة على تقسيم المجال الهندسي المعقد إلى أجزاء صغيرة وبسيطة ثم تقريب الحل داخل كل جزء بدوال متعددة الحدود. وقد شمل العمل تعريف الأشكال الهندسية الأساسية في أي بعد، وبناء فضاءات الدوال متعددة الحدود، وتعريف نقاط الربط الخاصة بهذه العناصر، ثم إثبات الخاصية الأساسية التي تضمن أن قيم الدالة عند هذه النقاط تحدد دالة وحيدة دون التباس. ولتحقيق ذلك كان من الضروري تطوير منظومة رياضية واسعة تشمل الفضاءات الشعاعية والفضاءات التآلفية والتحويلات الهندسية، مع التحقق من صحة كل تعريف وكل برهان آليًا وبشكل كامل.
تكمن أهمية هذا العمل في أنه يضع أسسًا رياضية موثوقة يمكن الاعتماد عليها لاحقًا للتحقق من صحة البرمجيات العلمية المستعملة في التطبيقات الحرجة، مما يساهم في تقليل مخاطر الأخطاء الخفية في الحسابات التي قد تكون لها آثار خطيرة على سلامة الإنسان والمنشآت. كما يوفر هذا البحث قاعدة علمية مفتوحة يمكن للباحثين البناء عليها مستقبلًا من أجل تطوير التحقق الشكلي الكامل لطرق المحاكاة العددية والبرامج الصناعية المرتبطة بها. وبذلك تمثل هذه الأطروحة خطوة مهمة نحو بناء ثقة حقيقية في الأنظمة الرقمية التي تعتمد عليها مجالات علمية وصناعية بالغة الحساسية.

Abstract of Thesis :Formal Proofs in Applied Mathematics :A Coq Formalization of Simplicial Lagrange Finite Elements
This thesis addresses a fundamental problem: software used to simulate safety-critical systems, such as bridges, medical devices, and self-driving cars, relies on complex mathematical computations, where even a minor programming or mathematical error can lead to extremely dangerous consequences. The central goal of the research is therefore to find a way to formally and unconditionally guarantee the correctness of the mathematical foundations underlying such software. To this end, the thesis adopts the methodology of formal proof, an approach that consists in translating mathematical proofs into a precise format that a specialized computer program can verify step by step, leaving no room for ambiguity or gaps in reasoning.
This work is part of a long-term scientific project aimed at fully verifying the correctness of scientific simulation programs used in highly sensitive fields such as aeronautics, energy, medicine, and civil engineering. Within this framework, the thesis makes two main contributions. The first is the formal verification of a fundamental theorem in the theory of multiple integrals, namely Tonelli’s theorem, which simplifies the computation of multi-variable integrals by reducing them to successive single-variable integrals, an essential tool in the study of equations describing physical phenomena.
The second and central contribution consists in building a complete formal specification of Lagrange finite elements, one of the most widely used tools in the numerical simulation of physical phenomena. This approach involves decomposing a complex geometric domain into small, simple pieces and approximating the solution within each piece using polynomial functions. The work encompassed the definition of reference geometric shapes in arbitrary dimensions, the construction of polynomial function spaces, the definition of the associated degrees of freedom, and the formal proof of the unisolvence property, which guarantees that the values of a function at the designated nodes uniquely determine it without ambiguity.
The significance of this work lies in its establishment of reliable mathematical foundations that can serve as a basis for verifying the correctness of scientific software used in critical applications, thereby contributing to the reduction of hidden computational errors that could have serious consequences for human safety and infrastructure. It also provides an open scientific foundation upon which future researchers can build, advancing the formal verification of numerical simulation methods and the industrial software associated with them. In this way, the thesis represents an important step toward building genuine trust in the digital systems upon which highly sensitive scientific and industrial fields depend.