Les assistants de preuve : comment avoir confiance en ses démonstrations
Orateur : Julien Narboux
ICube, Pôle API, Université de Strasbourg
Résumé : Cet exposé présentera une vue d’ensemble du domaine de la preuve formelle. On évoquera les questions suivantes :
- qu’est-ce qu’une preuve formelle ?
- qu’est-ce qu’un assistant de preuve ?
- pourquoi formaliser des preuves ?
- qu’est-ce qu’il est possible de prouver avec les assistants de preuve actuels ?
- quels sont les défis à relever ?
- comment utiliser la preuve formelle pour l’enseignement ?
L’histoire des mathématiques est riche en exemples de preuves fausses ou incomplètes. Par exemple, pendant des siècles des mathématiciens de renom ont cru que le fameux axiome des parallèles pouvait être déduit des autres axiomes d’Euclide. L’histoire de l’informatique, bien que beaucoup plus courte, n’est pas moins riche en exemple de bugs fameux. Après avoir présenté quelques exemples de preuves fausses et de bugs fameux, nous introduirons le domaine de la preuve formelle. Un assistant de preuve est un logiciel qui permet l’écriture et la vérification de preuves mathématiques ou de preuves de propriétés de programmes. L’assistant de preuve Coq est à la fois utilisé pour prouver des programmes et pour prouver des théorèmes mathématiques. Nous présenterons quelques exemples de preuves formelles à la fois dans le domaine des mathématiques et de l’informatique. Nous évoquerons la correspondance de Curry-Howard qui met en lumière le lien fondamental qui existe entre les preuves et les programmes. Pour terminer, je parlerai des expériences concernant l’utilisation de la preuve formelle pour l’enseignement du raisonnement mathématique.
Date et lieu : le Vendredi 20 Mai 2016 à 11h, salle 250, IUSTI