Résumé : Attention ! Exceptionnellement un mardi.
Les assistants de preuve sont des outils informatiques qui permettent de formaliser et vérifier tous les détails d’une preuve. Alors qu’ils sont développés et utilisés depuis longtemps par des informaticiens (notamment pour prouver qu’un programme fait bien ce qu’on attend de lui), leur adoption par des mathématiciens est beaucoup plus récente. Je décrirai à travers mon expérience personnelle ce que ces outils permettent déjà de faire, notamment pour des résultats niveau recherche, mais aussi les difficultés que pose leur utilisation pour un mathématicien. Et j’espère aussi dissiper quelques fantasmes !
Département de Mathématiques
Bâtiment 307
Faculté des Sciences d'Orsay Université Paris-Sud F-91405 Orsay Cedex Tél. : +33 (0) 1-69-15-79-56 
Département
Actualités
Les membres
Contacts
Présentation en images des maths à Orsay
Les Maths à Orsay de 1958 à nos jours
Diffusion des mathématiques
Offres d’emploi
Comité Parité du LMO
Fermeture du département
Fermeture du département
Laboratoire
|