###Patrick Massot (Université Paris Sud) ###Un mathématicien peut-il utiliser un logiciel de vérification de démonstration?

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

###Lieu LMJL, Salle des séminaires