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

After a short absence, we are happy to be able to organise again at IHES the Workshop Schlumberger. Organized by Thierry Coquand, current chairholder of the Schlumberger Chair for Mathematical Sciences, it will take place on June 15, 2022. The goal of this day will be to review recent developments in the typed lambda-calculus formalism and explore the limitations and possibilities of this approach.

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

The formalism of typed lambda-calculus and dependent types provides a notation system not only for mathematical objects (as was the case for the formalism used by Bourbaki) but also for mathematical proofs. This formalism is accurate enough to be represented on computers, and several interactive proof verification systems are based on this approach.

This subject has known spectacular developments in the last 15 years: non-trivial proofs have been formalized, such as the 4-color theorem, the Feit-Thompson theorem, or more recently, a complex lemma of P. Scholze (liquid tensor experiment).

In another direction, an unexpected connection between this formalism and the notion of higher-order topos has been highlighted.

Registration until June 12 on the dedicated webpage.

Invited speakers:

• 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