Nouveau workshop Schlumberger sur la formalisation des mathématiques
Visuel pour le workshop Schlumberger 2022 Événement

Workshop Schlumberger : types dépendants et formalisation des mathématiques

Après quelques années d’absence, l’IHES a le plaisir d’accueillir à nouveau le Workshop Schlumberger. Organisé par Thierry Coquand, titulaire de la chaire Schlumberger pour les sciences mathématiques, il aura lieu le 15 juin prochain. Le but de cette journée sera de faire le point sur les développements récents en formalisme du lambda-calcul typé, et d’explorer les limitations et possibilités de cette approche.

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.

Vous avez jusqu’au 12 juin inclus pour vous inscrire au Workshop Schlumberger 2022.

 

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 MassotLMO, Université Paris-Saclay