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
