Présentation
Ces dernières décennies, la complexité des preuves mathématiques a explosé, rendant compliquée leur vérification. Qui plus est, les mathématiciens se spécialisant, les personnes capables de vérifier chaque preuve sont de moins en moins nombreuses. De plus, on essaye aujourd’hui de prouver le bon comportement de programmes informatiques, par exemple dans le cas des systèmes embarqués dans des avions, où un bug aurait des effets dévastateur. Mais prouver un logiciel manuellement est extrèmement pénible et compliqué.
La question qui se pose alors est la suivante : comment vérifier automatiquement des preuves mathématiques ? Dans cet exposé, je vais présenter une des méthodes standard pour le faire : l’isomorphisme de Curry-Howard. Comme on va être amené à manipuler des preuves mathématiques, je vais aussi présenter comment on formalise les mathématiques avec des mathématiques en introduisant la notion de système logique.
