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.