Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieures

Denis-Charles Cisinski

Professeur, Universität Regensburg

Résumé

La logique des catégories supérieures (ou encore des ∞-catégories) est une variation de la théorie des types qui est homotopique par nature et dans laquelle la notion de catégorie est le concept primitif – celui que l'on ne définit jamais ! Une généralisation adéquate de l'axiome d'univalence de Voevodsky fait de cette théorie un langage très expressif, et ce, assez pour qu'il puisse produire ses propres interprétations sémantiques. Cela fournit un système de fondation des mathématiques au cœur duquel les concepts de la théorie des catégories ainsi que de la théorie de l'homotopie sont implémentés. Une logique des logiques. Une interprétation sémantique de cette logique est produite en mathématiques classiques par la théorie des ∞-catégories telle que développée par Joyal et Lurie. Une formulation en théorie des types dépendants, via la théorie de Riehl-Shulman, est l'objet d'un projet en cours de Buchholtz et Weinberger. Cette logique permet de formuler constructivement bien des théories considérées comme avancées (e.g. cohomologie étale des schémas dérivés ou non, catégories dérivées des faisceaux quasi cohérents) d'une manière proche de la pratique. C'est aussi une nouvelle manière d'appréhender la logique elle-même, de sorte que la distance entre syntaxe et sémantique est en apparence très significativement réduite : les logiques sont les termes d'un type, i.e. les objets d'une ∞-catégorie.

Denis-Charles Cisinski

Denis-Charles Cisinski est professeur de mathématiques à l'Universität Regensburg, en Allemagne. Il a occupé des postes permanents à l'université de Toulouse et à l'université Sorbonne-Paris-Nord, et est un ancien membre de l'Institut universitaire de France. Ses recherches portent sur l'algèbre homotopique, la théorie des catégories, la K-théorie et la cohomologie des schémas. Il est l'auteur de trois monographies : Les préfaisceaux comme modèles des types d'homotopie (2007), Triangulated categories of mixed motives (2019), et Higher categories and homotopical algebra (2019).

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Colloque - Formalisation des mathématiques et types dépendants - Riccardo Brasca : Progrès récents dans la formalisation de la théorie des nombres

Riccardo Brasca

Maître de conférences, université Paris Cité

Résumé

Dans cet exposé, nous discuterons de l'état actuel de la formalisation de la théorie des nombres moderne dans mathlib, la bibliothèque mathématique de Lean. Nous mettrons en avant les avancées récentes, les principaux défis qui ont été relevés, ainsi que les implications plus larges de ce travail. Nous aborderons également les perspectives d'avenir et les applications potentielles, en soulignant comment ces développements contribuent à l'écosystème croissant des mathématiques formalisées.

Riccardo Brasca

Riccardo Brasca a obtenu son doctorat à l'université de Milan (Italie) en 2012, avec une thèse portant sur les formes modulaires p-adiques. Après son doctorat, il a effectué deux postdoctorats, l'un au Max-Planck-Institut für Mathematik à Bonn et l'autre à l'École normale supérieure de Lyon. Depuis 2013, il est maître de conférences à l'université Paris-Cité et depuis 2020 il travaille en formalisation des mathématiques.

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondations

Pierre-Marie Pédrot

Chargé de recherche, Inria

Résumé

La preuve assistée par ordinateur séduit un public de plus en plus large. Jusque-là surreprésentée dans le domaine de l'informatique où elle était née, elle a commencé à susciter chez les mathématiciens un engouement certain. Néanmoins, cet appel d'air ne s'est pas fait sans incompréhension, les deux communautés ne partageant pas les mêmes arrière-fonds culturels.

Cet exposé présente un point de vue informaticien assumé sur les fondements d'un assistant à la preuve et de la pertinence même de cette question. Notre thèse s'appuie sur l'équivalence preuve-programme, qui sera utilisée aussi bien comme paradigme théorique que comme approche sociologique. Notre vision est à la fois pluraliste et moniste. Moniste, car le choix d'une fondation a de nombreuses conséquences pratiques sur l'utilisation d'un assistant à la preuve, il faut donc concevoir le meilleur système. Pluraliste, car nous ne croyons pas en un langage unique des mathématiques : chaque sous-domaine s'exprime dans des langages extrêmement différents. Cette disparité est bien connue des informaticiens, qui utilisent de nombreux langages de programmation sur le même ordinateur. Cette tension est résolue via la compilation. Nous exposerons quelques techniques inspirées de ce domaine et évoquerons un avenir radieux où cohabitent pléthore de systèmes de preuve de haut niveau.

Pierre-Marie Pédrot

Pierre-Marie Pédrot est un chercheur en informatique spécialisé dans la théorie des types et est l'un des principaux développeurs de l'assistant à la preuve Rocq. Son travail s'articule autour du contenu calculatoire de la logique au travers de la correspondance preuve-programme. En s'inspirant de comportements venus du monde de la programmation appelés « effets de bord », il a notamment conçu des modèles de la théorie de types qui étendent sa puissance expressive. En complément de ce volet théorique, une partie importante de son activité consiste à implémenter et maintenir Rocq, avec une certaine emphase sur les questions de passage à l'échelle.