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