La méthode des éléments finis est largement répandue pour résoudre des gammes d'équations aux dérivées partielles. Elle est basée sur un cadre mathématique bien connu et est implémentée dans de nombreux codes numériques. Notre objectif à relativement long terme est double : d'une part, prouver formellement en Coq que la méthode mathématique des éléments finis est "correcte", et d'autre part prouver, toujours en Coq et avec l'aide d'autres outils formels, que des parties de bibliothèques d'éléments finis en C++ sont "correctes". Le sens du mot "correct" est à préciser. Le but est d'avoir la plus grande confiance possible dans la méthode et son implémentation, en précisant/explicitant par exemple quelles sont les hypothèses nécessaires.
On commencera par une explication succincte, par un non spécialiste, de ce qu'un assistant de preuve (comme Coq) peut faire pour aider à prouver un théorème ou un programme. Ensuite, on illustrera brièvement la démarche, avec la preuve complète --mathématique et programme, faite par d'autres-- de l'équation des ondes 1D en différences finies. Enfin, on présentera quelques étapes vers la preuve de la méthode des éléments finis : la preuve du théorème de Lax--Milgram, la
construction de l'intégrale de Lebesgue et le théorème de Tonelli, pour finir sur la preuve en cours de l'unisolvance pour les éléments finis de Lagrange de degré k, sur un simplexe en dimension d.
Ce travail résulte d'une collaboration avec des informaticiennes, Sylvie Boldo (INRIA Saclay) et Micaela Mayero (LIPN, Paris 13) et un numéricien-informaticien François Clément (INRIA Paris). Florian Faissole (Mitsubishi Electric) et Houda Moucine (thèse en cours) ont contribué également.