Preuves formelles d'analyse fonctionnelle

La vérification formelle de preuves mathématiques à l'aide d'un ordinateur est une tâche nécessaire mais difficile. La recherche en assistant de preuve se situe en effet à la croisée des chemins entre les mathématiques pures, l'ingénierie logicielle et la logique. Le choix d'une théorie des types de base, d'un noyau fiable et d'outils orientés vers l’utilisatrice ou l’utilisateur permet de rendre les preuves formelles aussi proches que possible des intuitions mathématiques.