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.
Un mathématicien peut-il utiliser un logiciel de vérification de démonstration ?
- Se connecter pour poster des commentaires
Nom de l'orateur
Patrick Massot
Etablissement de l'orateur
Université Paris-Sud
Date et heure de l'exposé
Lieu de l'exposé
Salle des séminaires