Workshop Schlumberger :
Types dépendants et Formalisation des mathématiques

Le formalisme du lambda-calcul typé et des types dépendants fournit un système de notation non seulement pour les objets mathématiques (comme c’était le cas pour le formalisme utilisé par Bourbaki), mais également pour les preuves mathématiques. Ce formalisme est assez précis pour être représenté sur ordinateurs, et plusieurs systèmes interactifs de verification de preuves se fondent sur cette approche.

Ce sujet a connu ces 15 dernières  années des développements spectaculaires : des preuves non triviales ont ainsi été formalisées, comme celle du théorème des 4 couleurs, ou le théorème de Feit-Thompson, ou plus récemment, un lemme complexe de P. Scholze (liquid tensor experiment).

Dans une autre direction, un rapprochement inattendu entre ce formalisme et la notion de topos d'ordre supérieur a été mis en évidence.

Organisée par Thierry Coquand, titulaire de la chaire Schlumberger pour les sciences mathématiques à l'IHES, le but de ce cette journée est de faire le point sur ces développements récents, et d’explorer les limitations et possibilités de cette approche.

Conférenciers invités :

• Benedikt Ahrens, Delft University of Technology
• Anthony Bordg, University of Cambridge
• Cyril Cohen, INRIA
• Georges Gonthier, INRIA
• Assia Mahboubi, INRIA
• Patrick Massot, LMO, Université Paris-Saclay