Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation

Plan du cours :

paradoxe de Girard avec un type de tous les types ;

différence avec le paradoxe de Russell ;

univers comme principe de réflexion ;

preuve algébrique de canonicité avec la technique du collage à la Artin et preuve de normalisation ;

application à la vérification des preuves.

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

02 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèles

Plan du cours :

Curry-Howard ;

déduction naturelle de Gentzen ;

définitions inductives suivant Martin-Löf ;

présentation algébrique de la théorie des types et modèle des termes comme modèle initial ;

quelques exemples de modèles, en particulier modèle ensembliste et modèles de préfaisceaux.

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

01 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn

Plan du cours :

théorie des types de Russell ;

notation du λ-calcul de Church pour les fonctions ;

théorie des types simples et système HOL ;

introduction aux types dépendants, système AUTOMATH ;

traitement uniforme des objets et des preuves mathématiques ;

vérification des preuves comme vérification des types.

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration

Ré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 Curry-Howard entre types et propositions. Certains résultats plus récents indiquent que ce formalisme permet de formuler des propriétés nouvelles sur une des notions de base de la mathématique : la notion d'égalité, avec un rapprochement inattendu entre des questions de base de la logique et de la théorie abstraite de l'homotopie.

Cette leçon retracera l'histoire récente de ces découvertes, aussi bien autour de la vérification des preuves sur ordinateur que de la synergie qui est en train de s'établir entre la théorie des types dépendants et la théorie de l'homotopie.