Séance Séminaire

Séminaire de Recherche en Didactique et Epistémologie des Mathématiques

Les assistants de preuve et applications à l'apprentissage du raisonnement mathématique

Cet exposé présentera une vue d'ensemble du domaine de la preuve formelle et son application en géométrie. 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. Après avoir présenté quelques exemples de preuves fausses et de bugs,nous présenterons 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. En particulier, nous présenterons la bibliothèque GeoCoq sur les fondements de la géométrie. Enfin, nous évoquerons les motivations et problématiques pour l'utilisation de la preuve formelle pour l'enseignement du raisonnement mathématique.