Types Dépendants et Formalisation des Mathématiques

Explorez les types dépendants et leur application à la formalisation des mathématiques dans ce workshop de 4 heures 51 minutes organisé par l'Institut des Hautes Etudes Scientifiques. Découvrez comment le formalisme du lambda-calcul typé et des types dépendants offre un système de notation précis pour représenter non seulement les objets mathématiques, mais également les preuves mathématiques sur ordinateur. Apprenez les développements spectaculaires de ces 15 dernières années, incluant la formalisation de preuves non triviales comme le théorème des 4 couleurs, le théorème de Feit-Thompson, et un lemme complexe de P. Scholze dans le cadre du liquid tensor experiment. Examinez le rapprochement inattendu entre ce formalisme et la notion de topos d'ordre supérieur. Suivez les interventions d'experts couvrant la formalisation mathématique et les types dépendants du point de vue pratique, les approches alternatives sans types dépendants, les encodages fonctionnels des mathématiques, le principe d'univalence pour le transfert de raisonnement à travers les équivalences, et l'utilisation d'Hierarchy Builder. Organisé par Thierry Coquand, titulaire de la chaire Schlumberger pour les sciences mathématiques, ce workshop présente les fondements théoriques et les applications pratiques des systèmes interactifs de vérification de preuves.