MALINCA, ou comment vérifier automatiquement les théorèmes sans avoir à les réécrire

Carlos Simpson, directeur de recherche CNRS au Laboratoire Jean-Alexandre Dieudonné - LJAD (CNRS/Université Côte d’Azur), ainsi que des scientifiques de l’Institut de recherche en informatique fondamentale - IRIF (CNRS/Université Paris Cité) et du Laboratoire lorrain de recherche en informatique et ses applications - LORIA (CNRS/Université de Lorraine) ont obtenu un financement ERC Synergy pour combler l’écart entre une démonstration mathématique et les logiciels d’assistance à la preuve. Il s’agit de permettre à ces derniers de comprendre directement des textes, par exemple d’algèbre, tels qu’on les trouve dans les ouvrages académiques.

Lire l'article complet