OLYMPUS DIGITAL CAMERA
Cet article introductif fait écho aux deux exposés donnés par Thierry Coquand et Thomas C. Hales au séminaire Bourbaki du 21 juin 2014. Ces exposés sont tous deux consacrés à des développements récents liés à la preuve formelle, une discipline au confluent entre mathématiques et informatique.
Les vidéos de ces exposés sont disponibles en ligne : ici pour celui de Thierry Coquand et ici pour celui de Thomas C. Hales.
ÉCRIT PAR
Assia Mahboubi
Directrice de recherche - Inria, Équipe Gallinette, Nantes
Il est possible d’utiliser des commandes LaTeX pour rédiger des commentaires — mais nous ne recommandons pas d’en abuser ! Les formules mathématiques doivent être composées avec les balises .
Par exemple, on pourra écrire que sont les deux solutions complexes de l’équation .
Si vous souhaitez ajouter une figure ou déposer un fichier ou pour toute autre question, merci de vous adresser au secrétariat.