Collège De France (général)

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstrationRésuméLa théorie des types a été introduite par Bertrand Russell pour éviter les paradoxes qui apparaissent en mathématique si l'on utilise de manière trop naïve la notion de collection d'objets. Cette notion de types a été raffinée par la notion de type dépendant, dans le but de représenter les preuves mathématiques sur ordinateur, et de pouvoir ainsi vérifier la correction de ces preuves. Cette idée d'utiliser ainsi l'ordinateur connaît depuis quelques années un grand développement (vérification de la preuve du théorème de l'ordre impair ou, plus récemment, d'un résultat non trivial de Peter Scholze). Indépendamment de ce rôle important pour la formalisation des preuves mathématiques, la notion de type dépendant présente un intérêt conceptuel intrinsèque en logique et informatique, à travers la correspondance de C