Informatique et sciences numériques (2024-2025) - Thierry Coquand

Collège de France
  • 0.0 (0)
  • COURSES
  • UPDATED WEEKLY

Informatique et sciences numériques (2024-2025) Thierry Coquand Année 2024-2025 Chaire annuelle Présentation de la chaire Créée en partenariat avec Inria, la chaire annuelle Informatique et sciences numériques marque une volonté commune de faire valoir l'importance de cette discipline scientifique et la nécessité de lui octroyer une place pleine et entière. Théorie des types dépendants et formalisation des mathématiques La théorie des types a été introduite par Bertrand Russell pour éviter les paradoxes qui apparaissent en mathématique si l'on utilise de manière trop naïve la notion de collection d'objets. Cette notion de types a été raffinée par la notion de type dépendant, dans le but de représenter les preuves mathématiques sur ordinateur, et de pouvoir ainsi vérifier la correction de ces preuves. Cette idée d'utiliser ainsi l'ordinateur connaît depuis quelques années un grand développement (vérification de la preuve du théorème de l'ordre impair ou, plus récemment, d'un résultat non trivial de Peter Scholze). Indépendamment de ce rôle important pour la formalisation des preuves mathématiques, la notion de types dépendants présente aussi un intérêt conceptuel intrinsèque en logique et informatique, à travers la correspondance de Curry-Howard entre types et propositions. De plus, Voevodsky a pu donner à la notion de type dépendant une sémantique naturelle en théorie abstraite de l'homotopie, et ce rapprochement inattendu entre des questions de base de la logique et de la théorie de l'homotopie apparaît fondamental. Le cours que nous proposons pour l'année 2024–2025 s'inscrit dans ce foisonnement d'idées autour des théories des types. Dans la première partie, on présentera en détail la théorie des types dépendants et ces propriétés métamathématiques qui justifient son utilisation pour la vérification des preuves sur ordinateur. La deuxième partie du cours sera consacrée à la synergie qui est en train de s'établir entre cette théorie et la théorie de l'homotopie. Biographie Après des études à l'École normale supérieure de Paris, Thierry Coquand passe sa thèse d'informatique théorique en 1985, introduisant la théorie des constructions, formalisme utilisé dans plusieurs systèmes d'assistants à la démonstration. Depuis 1996, il est professeur en informatique à l'université de Göteborg, en Suède. Ses recherches concernent les mathématiques constructives, la théorie des types et ses applications pour la représentation des preuves sur ordinateur, et la sémantique des langages de programmation. Il a été coorganisateur, avec Vladimir Voevodsky et Steve Awodey, de l'année spéciale 2012-2013 à l'Institute of Advanced Study, Princeton, sur les Univalent Foundations of Mathematics. Ses travaux récents ont pour but de donner un sens effectif à l'axiome d'univalence, introduit par Voevodsky, et aux modèles de faisceaux (topos d'ordre supérieur). Pour ses travaux en logique, il a eu le Kurt Godel Centenary Research Prize 2008, et pour ses travaux sur les assistants de preuve, il a reçu, en collaboration, le ACM SIGPLAN Programming Languages Software Award, 2013.

  1. 06/02/2025

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

    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).

    44 min

  2. 06/02/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

    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.

    47 min

  3. 06/02/2025

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

    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.

    47 min

  4. 06/02/2025

    Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandis

    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 - Assia Mahboubi : Preuves formelles mutatis mutandis Assia Mahboubi Directrice de recherche, Inria Résumé Comme c'est le cas dans la littérature, l'ajout d'un concept mathématique à un corpus de bibliothèques formelles donne typiquement lieu à plusieurs variantes de définitions, le plus souvent équivalentes mais pas toujours. Malheureusement, la transposition des preuves formelles de théorèmes associées à ces différentes variantes est alors très pédestre, alors que sur papier, ces étapes triviales resteraient implicites. Cette nécessaire bureaucratie est de fait un frein notoire à la formalisation de mathématiques « intéressantes ». Dans cet exposé nous discuterons la construction d'un outil de transfert de preuves en théorie des types. Base sur une généralisation de la traduction de paramétricité de Tabareau-Tanter-Sozeau, cette approche est utilisable dans des prouveurs comme Rocq ou Lean. Il s'agit d'un travail en collaboration avec Cyril Cohen et Enzo Crance. Assia Mahboubi Assia Mahboubi est directrice de recherche à l'Inria, au sein du laboratoire des Sciences du Numérique de Nantes. Elle occupe aussi une chaire dans le département de mathématiques de la Vrije Universiteit Amsterdam, aux Pays-Bas.

    50 min

  5. 06/02/2025

    Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées

    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 - Antoine Chambert-Loir : Sur la formalisation des puissances divisées Antoine Chambert-Loir Professeur, université Paris Cité Résumé Je ferai le point sur un travail de formalisation de la théorie des puissances divisées que je mène avec María-Inés de Frutos Fernández. Découvert par Cartan dans un contexte de topologie algébrique, cet outil algébrique a été développé dans les années 60 par Roby et est au cœur de la construction de la cohomologie cristalline. J'évoquerai en particulier la construction des puissances divisées sur l'idéal d'augmentation de l'algèbre à puissances divisées. Antoine Chambert-Loir Les travaux de recherche d'Antoine Chambert-Loir s'inscrivent le plus souvent en géométrie diophantienne (question de Manin sur les points de hauteur bornée) et en géométrie non archimédienne (construction d'une théorie de formes différentielles et courants réels). Depuis 2021, il s'intéresse à la formalisation mathématique, en concentrant son attention sur des résultats peu spectaculaires au premier abord, comme la théorie des actions de groupes ou celle des puissances divisées.

    45 min

  6. 05/19/2025

    08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types

    Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types Plan du cours : modalités exactes à gauche ; application pour construire des nouveaux modèles de la théorie des types ; non prouvabilité de la thèse de Church et du choix dénombrable ; structure de modèle de Quillen et modèle constructif de la notion de types d'homotopie.

    1h 18m

  7. 05/12/2025

    07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie

    Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie Plan du cours : opération de débouclage des groupes ; un exemple paradigmatique de définition de types qui ne sont pas des ensembles, les espaces d'Eilenberg-MacLane ; utilisation de ces types pour définir les groupes de cohomologie.

    1h 11m

  8. 05/05/2025

    06 - Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d'univalence

    Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 06 - Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d'univalence Plan du cours : modèle de Voevodsky des ensembles simpliciaux et caractère non effectif de ces modèles ; modèles effectifs avec ensembles cubiques ; application à une définition de structure de modèle la Quillen sur certains modèles de préfaisceaux ; définition constructive des types d'homotopie des espaces topologiques.

    1h 16m
See All (14)

About

Informatique et sciences numériques (2024-2025) Thierry Coquand Année 2024-2025 Chaire annuelle Présentation de la chaire Créée en partenariat avec Inria, la chaire annuelle Informatique et sciences numériques marque une volonté commune de faire valoir l'importance de cette discipline scientifique et la nécessité de lui octroyer une place pleine et entière. Théorie des types dépendants et formalisation des mathématiques La théorie des types a été introduite par Bertrand Russell pour éviter les paradoxes qui apparaissent en mathématique si l'on utilise de manière trop naïve la notion de collection d'objets. Cette notion de types a été raffinée par la notion de type dépendant, dans le but de représenter les preuves mathématiques sur ordinateur, et de pouvoir ainsi vérifier la correction de ces preuves. Cette idée d'utiliser ainsi l'ordinateur connaît depuis quelques années un grand développement (vérification de la preuve du théorème de l'ordre impair ou, plus récemment, d'un résultat non trivial de Peter Scholze). Indépendamment de ce rôle important pour la formalisation des preuves mathématiques, la notion de types dépendants présente aussi un intérêt conceptuel intrinsèque en logique et informatique, à travers la correspondance de Curry-Howard entre types et propositions. De plus, Voevodsky a pu donner à la notion de type dépendant une sémantique naturelle en théorie abstraite de l'homotopie, et ce rapprochement inattendu entre des questions de base de la logique et de la théorie de l'homotopie apparaît fondamental. Le cours que nous proposons pour l'année 2024–2025 s'inscrit dans ce foisonnement d'idées autour des théories des types. Dans la première partie, on présentera en détail la théorie des types dépendants et ces propriétés métamathématiques qui justifient son utilisation pour la vérification des preuves sur ordinateur. La deuxième partie du cours sera consacrée à la synergie qui est en train de s'établir entre cette théorie et la théorie de l'homotopie. Biographie Après des études à l'École normale supérieure de Paris, Thierry Coquand passe sa thèse d'informatique théorique en 1985, introduisant la théorie des constructions, formalisme utilisé dans plusieurs systèmes d'assistants à la démonstration. Depuis 1996, il est professeur en informatique à l'université de Göteborg, en Suède. Ses recherches concernent les mathématiques constructives, la théorie des types et ses applications pour la représentation des preuves sur ordinateur, et la sémantique des langages de programmation. Il a été coorganisateur, avec Vladimir Voevodsky et Steve Awodey, de l'année spéciale 2012-2013 à l'Institute of Advanced Study, Princeton, sur les Univalent Foundations of Mathematics. Ses travaux récents ont pour but de donner un sens effectif à l'axiome d'univalence, introduit par Voevodsky, et aux modèles de faisceaux (topos d'ordre supérieur). Pour ses travaux en logique, il a eu le Kurt Godel Centenary Research Prize 2008, et pour ses travaux sur les assistants de preuve, il a reçu, en collaboration, le ACM SIGPLAN Programming Languages Software Award, 2013.

Information