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

mercredi 15 juin 2022, 09:00 → 18:30 Europe/Paris

Centre de conférences Marilyn et James Simons (Le Bois-Marie)

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

09:00 Café d'accueil

1 Formalisation mathématique et types dépendants : Le point vue d'un utilisateur mathématicien (T: 45min + Q: 15)

Dans cet exposé je passerai en revue les surprises bonnes et moins bonnes je j'ai rencontrées en formalisant des mathématiques modernes en théorie des types dépendants.

Orateur: Prof. Patrick MASSOT (LMO, Université Paris-Saclay)

Vidéo

10:30 Pause café

2 How to Do Maths Without Dependent Types (T: 45 min + Q: 15min)

What can be done when formalizing mathematics without dependent types? I will give you new insights into this question by exploring the capability and possible limitations of the Isabelle/HOL proof assistant. I will explain what we learnt formalizing Grothendieck's schemes using only Isabelle's module system called "locales".

Orateur: Prof. Anthony BORDG (University of Cambridge)

Vidéo

12:00 Déjeuner

3 Functional Encodings of Mathematics (T: 45 min + Q: 15min)

A remarkable feature of logics based on typed lambda calculus is that they allow embedding functional programs in the representation of mathematical knowledge.
These can be used to animate formal theories and make them behave, in part, as a working mathematician would expect. Examples of such functional encodings have played a key part in several large formal proofs, such as this of the Four-Color and Odd Order theorems.

Orateur: Prof. Georges GONTHIER (INRIA)

Vidéo

4 Verified Computational Mathematics (T: 45min + Q: 15min)

Computers are widely used as observation instruments for testing and refining conjectures, in a broad range of mathematical areas. They actually even substantiate actual proof steps in published proofs. In particular, a large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation, and the potential of proof assistants based on dependent types.

Orateur: Prof. Assia MAHBOUBI (INRIA)

15:30 Pause café

5 Le principe d'univalence: le transfer du raisonnement à travers les equivalence (T: 45min + Q: 15min)

Le raisonnement à équivalence près est omniprésent en mathématique, et les mathématiciens le font implicitement. Pour les mathématiques sur ordinateurs, ce n'est pas si simple : il faut donner tous les détails explicitement. C'est pour cela que Voevodsky a créé les fondements univalents, avec l'objectif de mécaniser le transfer du raisonnement à travers les équivalences. Je présenterai notre travail (avec North, Shulman et Tsementzis) sur le principe d'univalence en fondements univalents, qui met en pratique la vision de Voevodsky.

Orateur: Prof. Benedikt AHRENS (Delft University of Technology)

Vidéo

6 Hierarchy Builder (T: 45min + Q: 15min)

Libraries of machine-checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately, the language of Type Theory and the features provided by modern proof assistants make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between different inference mechanisms. To this, one may add the concerns about performance and about the usability, by a non-expert, of the final hierarchy.

Hierarchy Builder (HB), as implemented inside the Coq proof assistant, gives library designers a language to describe the building blocks of algebraic structures and to assemble them into a hierarchy. Similarly, it provides the final user tools to build instances of structures and to inform the system how to take advantage of this knowledge during type inference. Finally, HB lets library designers improve the usability of their library by providing alternative interfaces to the primitive ones, a feature that is also useful to accommodate changes to the hierarchy without breaking user code.

This is joint work with Kazuhiko Sakaguchi and Enrico Tassi.

Orateur: Prof. Cyril COHEN (INRIA)

Vidéo