Colloquium : Patrick Massot, 18 octobre 2018

Titre : Un mathématicien peut-il utiliser un logiciel de vérification de démonstration?

Nom de l'orateur : Patrick Massot

Établissement de l'orateur : Université Paris-Sud

Lieu de l'exposé : Salle des séminaires

Date et heure de l'exposé : 18 octobre 2018 - 17h15

Les logiciels de vérification de démonstrations existent depuis la fin des années 60 et ont fait de grands progrès ces dernières années. On pourrait imaginer que les mathématiciens les utilisent, que ce soit à petite échelle ou pour vérifier des théories très techniques, ou encore pour enseigner la notion de démonstration. Cependant, presque aucun mathématicien ne le fait. On sait depuis la vérification en 2012 du théorème de Feit-Thompson que, entre les mains d’informathématiciens experts, ces logiciels peuvent vérifier une démonstration longue et compliquée mais ne faisant intervenir que des objets simples à définir. Dans cet exposé, je rendrai compte d’expériences en cours où des mathématiciens, sans formation en informatique théorique, essayent de manipuler des objets mathématiques sophistiqués dans le logiciel de vérification Lean.

type actualité
Date de début de l'actualité
Date de fin de l'actualité