Colloques du Collège de France - Collège de France

Antoine Georges

Physique de la matière condensée

Année 2024-2025

Colloque : Recent Advances and Applications of Diagrammatic Monte Carlo for Fermions

Olivier Parcollet : Learning Feynman Diagrams with Tensor Trains

Olivier Parcollet

Flatiron Institute

Résumé

The real-time dynamics of interacting quantum systems remains a major challenge in computational quantum physics. Surprisingly, high-order perturbative expansions have recently emerged as a promising approach to address this question, even in strong coupling regimes and out-of-equilibrium situations. I will present the cornerstone of these approaches: parsimonious representations of diagrammatic expansions made of tensor networks and revealed by a new generation of algorithms. Finally, I will discuss applications to mesoscopic systems, along with the future perspectives and challenges in this field.

Antoine Georges

Physique de la matière condensée

Année 2024-2025

Colloque : Recent Advances and Applications of Diagrammatic Monte Carlo for Fermions

Michel Ferrero : Origin and Fate of the Pseudogap in the Doped Hubbard Model: A Diagrammatic Monte Carlo Study

Michel Ferrero

École Polytechnique, CPHT, Collège de France

Résumé

In this seminar, I will introduce the diagrammatic Monte Carlo method and discuss its application to the two-dimensional Hubbard model at finite temperature. The results obtained through this approach are controlled and, importantly, address the infinite-size limit of the model, thus yielding physical quantities with arbitrary momentum resolution. This enables a detailed investigation of the impact of electronic correlations on the spectral properties, with a particular focus on the Fermi surface topology and the pseudogap regime. We demonstrate the selective suppression of quasiparticle excitations near the antinodal regions due to the development of magnetic correlations, observed both in the weak coupling regime with a large correlation length and in the strong coupling regime with a shorter correlation length. Furthermore, I will discuss how a modified spin-fluctuation theory can account for these findings. Finally, the evolution of the pseudogap regime with decreasing temperature will be examined, revealing its instability and eventual transition into an ordered stripe phase, consistent with ground-state calculations.

Antoine Georges

Physique de la matière condensée

Année 2024-2025

Colloque : Recent Advances and Applications of Diagrammatic Monte Carlo for Fermions

Thomas Schäfer : Bridging the Gap of Multi-Method, Multi-Messenger Studies from Known to Unknown Fluctuations

Thomas Schäfer

Max Planck Institute for Solid State Research, Stuttgart

Résumé

The strong mutual repulsion of electrons is responsible for some of the most interesting phenomena in contemporary condensed matter physics, where examples range from unconventional high-temperature superconductivity, over quantum criticality to Mott metal-to-insulator transitions. Despite the intense research on the quantum many-body problem over the last decades, many of its aspects have not yet been fully understood. Recent progress, however, has been achieved by the application of so-called multi-method, multi-messenger studies of the most fundamental model for electronic correlations, the Hubbard model [1,2].

In the first part of the talk, I will present such a study of the half-filled two-dimensional Hubbard model on a simple square lattice at small values of the local Coulomb interaction [1]. I will demonstrate that the footprints of spin fluctuations can be tracked by a rich series of crossovers in multiple observables by multiple numerical techniques. In the second part of the talk, I will show how one can determine which fluctuation channel (charge, spin, particle-particle) is responsible for spectral properties such as the pseudogap in the strong coupling regime, directly relevant to cuprates. For this I will introduce the so-called "fluctuation diagnostics" approach [3,4], which can be utilized on top of diverse numerical methods, making it a helpful tool for future multi-method studies of strongly correlated phenomena.

Références

[1] Thomas Schäfer, Nils Wentzell, Fedor Šimkovic IV, Yuan-Yao He, Cornelia Hille, Marcel Klett, Christian J. Eckhardt, Behnam Arzhang, Viktor Harkov, François-Marie Le Régent, Alfred Kirsch, Yan Wang, Aaram J. Kim, Evgeny Kozik, Evgeny A. Stepanov, Anna Kauch, Sabine Andergassen, Philipp Hansmann, Daniel Rohe, Yuri M. Vilk, James P. F. LeBlanc, Shiwei Zhang, A.-M. S. Tremblay, Michel Ferrero, Olivier Parcollet, Antoine Georges, "Tracking the Footprints of Spin Fluctuations: A Multi-Method, Multi-Messenger Study of the Two-Dimensional Hubbard Model", Phys. Rev. X, 11, 011058 (2021).

[2] Alexander Wietek, Riccardo Rossi, Fedor Šimkovic IV, Marcel Klett, Philipp Hansmann, Michel Ferrero, E. Miles Stoudenmire, Thomas Schäfer, and Antoine Georges, "Mott insulating states with competing orders in the triangular lattice Hubbard model", Phys. Rev. X, 11, 041013 (2021).

[3] O. Gunnarsson, T. Schäfer, J. LeBlanc, E. Gull, J. Merino, G. Sangiovanni, G. Rohringer, and A. Toschi, "Fluctuation Diagnostics of the Electron Self-Energy: Origin of the Pseudogap Physics", Phys. Rev. Lett., 114, 236402 (2015).

[4] Thomas Schäfer and Alessandro Toschi, "How to read between the lines of electronic spectra: the diagnostics of fluctuations in strongly correlated electron systems", J. Phys.: Condens. Matter, 33, 214001 (2021).

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.

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.

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.

Claudine Tiercelin

Métaphysique et philosophie de la connaissance

Année 2024-2025

Colloque - Implications philosophiques de l'IA

Carina Prunkl : L'IA en tant que bureaucratie

Carina Prunkl

Université d'Utrecht

Résumé

Le processus décisionnel piloté par l'IA est souvent évalué à l'aune du jugement humain individuel – les algorithmes sont-ils plus rapides, plus justes ou moins biaisés que les humains ? Dans cet exposé, je remets en question ce cadre, en soutenant que la classe de comparaison la plus appropriée pour la prise de décision pilotée par l'IA n'est pas le jugement humain individuel, mais la prise de décision bureaucratique. Comme les systèmes bureaucratiques, la prise de décision par l'IA dépend de la quantification, de la standardisation, de l'autorité dépersonnalisée et des tâches spécialisées. Elle ne supprime pas entièrement le pouvoir discrétionnaire de l'homme, mais le répartit tout au long du processus, depuis la sélection des données et la conception du modèle jusqu'à la mise en œuvre et la supervision. Les bureaucraties et l'IA visent toutes deux la cohérence et l'impartialité, mais elles sont également critiquées pour leur opacité, leur rigidité et leur insensibilité au contexte. Dans cet exposé, je montrerai comment le fait de passer d'un cadre humain contre machine à un cadre algorithme contre bureaucratie ouvre des voies nouvelles et plus productives pour réfléchir à la responsabilité, au pouvoir discrétionnaire et à la légitimité dans les systèmes d'IA.

--

Colloque organisé par Jacques-Henri Vollet, codirecteur du Groupe de recherche en épistémologie (GRE) au Collège de France, et Alexandre Declos, directeur du Groupe d'études en métaphysique (GEM).

Présentation

Ce colloque vise à explorer les implications philosophiques de l'intelligence artificielle (IA) à travers trois axes majeurs : épistémologique, esthétique et éthique.

Sur le plan épistémologique, nous interrogerons la nature de la connaissance produite par l'IA : peut-elle être qualifiée de véritable connaissance ou s'agit-il d'une simple corrélation statistique ? Quelles conséquences l'IA a-t-elle sur les notions de justification, de vérité et d'explicabilité en science et dans la prise de décision ?

D'un point de vue esthétique, nous examinerons le statut artistique et la valeur esthétique des productions de l'IA. Peut-on attribuer une forme d'intentionnalité ou d'auctorialité à ces systèmes ? L'IA peut-elle créer de l'art ? N'est-elle qu'un outil artistique parmi d'autres ?

Enfin, l'axe éthique portera sur les responsabilités associées au développement et à l'usage de l'IA. Comment assurer une IA alignée sur des valeurs humaines ? Quels sont les défis liés à la partialité algorithmique, à la surveillance de masse et aux impacts socio-économiques de l'automatisation ?

Ce colloque réunira des philosophes, des chercheurs en intelligence artificielle et des experts en éthique du numérique afin de proposer une réflexion interdisciplinaire sur ces enjeux cruciaux.

Claudine Tiercelin

Métaphysique et philosophie de la connaissance

Année 2024-2025

Colloque - Implications philosophiques de l'IA

Artūrs Logins : L'IA explicable et la philosophie des raisons

Artūrs Logins

Université Laval

Résumé

Il s'agira de réfléchir à l'opacité des modèles d'IA et à la manière dont les approches dites « explicables » (XAI), souvent post-hoc, pourraient être améliorées en déplaçant l'attention de l'explication causale vers l'explication par des raisons.

--

Colloque organisé par Jacques-Henri Vollet, codirecteur du Groupe de recherche en épistémologie (GRE) au Collège de France, et Alexandre Declos, directeur du Groupe d'études en métaphysique (GEM).

Présentation

Ce colloque vise à explorer les implications philosophiques de l'intelligence artificielle (IA) à travers trois axes majeurs : épistémologique, esthétique et éthique.

Sur le plan épistémologique, nous interrogerons la nature de la connaissance produite par l'IA : peut-elle être qualifiée de véritable connaissance ou s'agit-il d'une simple corrélation statistique ? Quelles conséquences l'IA a-t-elle sur les notions de justification, de vérité et d'explicabilité en science et dans la prise de décision ?

D'un point de vue esthétique, nous examinerons le statut artistique et la valeur esthétique des productions de l'IA. Peut-on attribuer une forme d'intentionnalité ou d'auctorialité à ces systèmes ? L'IA peut-elle créer de l'art ? N'est-elle qu'un outil artistique parmi d'autres ?

Enfin, l'axe éthique portera sur les responsabilités associées au développement et à l'usage de l'IA. Comment assurer une IA alignée sur des valeurs humaines ? Quels sont les défis liés à la partialité algorithmique, à la surveillance de masse et aux impacts socio-économiques de l'automatisation ?

Ce colloque réunira des philosophes, des chercheurs en intelligence artificielle et des experts en éthique du numérique afin de proposer une réflexion interdisciplinaire sur ces enjeux cruciaux.