|
14-14 oct. 2025 Paris (France)
|
programmeProgramme provisoire
10h - 10h45 : Formalisation Mathématique en Lean, Filippo A. E. Nuccio, INRIA et Institut Camille Jordan (Université Jean Monnet Saint-Étienne) Après une introduction générale aux mathématiques assistées par ordinateur, je me concentrerai sur l'assistant de preuve Lean et sur sa bibliothèque de mathématiques formalisées Mathlib. Je montrerai des exemples plus ou moins élémentaires et je parlerai de quelque projet qui s'est développé, ou est en train de se développer, autour de Mathlib (entre autres, Le Liquid Tensor Experiment, le projet du retournement de la sphère, le projet du théorème de Carlson, du dernier théorème de Fermat, etc...). Je terminerai avec une discussion de comment la formalisation pourrait modifier notre approche aux mathématiques dans le années qui viennent. 10h45 - 11h30 : IA et mathématiques, Gabriel Peyré, CNRS et ENS Cet exposé s’organise en deux parties. La première sera consacrée aux mathématiques pour l’IA : nous verrons comment des outils mathématiques sont mobilisés pour concevoir, analyser et améliorer les architectures de réseaux de neurones, les algorithmes d’entraînement, et plus généralement les fondements des systèmes d’apprentissage automatique. La seconde partie portera sur l’IA pour les mathématiques. Les développements récents autour des grands modèles de langage (LLMs), qui exploitent ces réseaux génératifs pour effectuer des raisonnements, placent les mathématiques au centre des avancées actuelles. L’entraînement et l’utilisation de ces modèles soulèvent des questions touchant à la fois à l’écriture des mathématiques en langage naturel (informel) et à leur formalisation dans des langages structurés comme Lean. Cette double interaction ouvre de nouvelles perspectives pour la recherche mathématique assistée par l’IA, tout en posant des questions importantes sur l’évolution des métiers d’enseignant et de chercheur en mathématiques. 11h30 - 12h15 : Défis de calcul pour comprendre le rythme cardiaque, les projets MICROCARD, Yves Coudière, Institut de Mathématiques de Bordeaux (Université de Bordeaux), IHU Liryc et Inria Environ la moitié des décès liés aux maladies cardiovasculaires sont dus à un trouble du rythme cardiaque. En effet, chaque battement du coeur est synchronisé par la propagation rapide (moins de 100 ms) d'une impulsion électrique à travers l'ensemble du muscle cardiaque. Des modèles classiques de réaction diffusion sont déjà très utilisés pour mieux comprendre cette propagation et leur simulation numérique repose sur l'utilisation de HPC de manière assez maîtrisée. Néanmoins, ces modèles, homogénéisés, ne sont pas assez précis pour décrire des arythmies dont l'origine est recherchée à l'échelle cellulaire ou inférieure. L'objectif des projets MICROCARD est de construire un modèle numérique décrivant chacune des cellules cardiaques (de l'ordre de quelques milliards). Nous estimons que le problème à résoudre aura 10 000 fois plus d'inconnues qu'avec un problème homegénéisé. Pour cela, nous proposons d'utiliser les ordinateurs de type exascale qui sont en cours de conception et installation en Europe et nous avons mis en place un consortium international et pluridisciplinaire, en ingénierie biomédicale, mathématiques, informatique. Je raconterais le travail réalisé ou en cours dans les projets MICROCARD (2021-2024) et MICROCARD-2 (2024-2027). Dans ceux-ci, nous travaillons conjointement sur des schémas d'approximations, la création de maillage, le partitionnement de graphe, la résolution des systèmes linéaires, la gestion de l'énergie, etc. In fine, nous cherchons à développer un programme qui pourra être utilisé à l'échelle exascale, en orchestrant ces différents aspects du mieux possible.
12h15 - 14h : Pause
14h - 14h45 : Calcul quantique : principe et perspectives, Mi-Song Dupuy, LJLL, Sorbonne Université Le calcul quantique est une nouvelle approche de l’informatique, basée sur les principes de la mécanique quantique. Contrairement aux bits classiques, les qubits peuvent exister en superposition d’états, évoluant selon une dynamique unitaire, déterministe et réversible jusqu’à ce qu’une mesure soit effectuée. Des notions fondamentales comme le théorème de non-clonage, qui interdit la copie d’un état quantique inconnu, et l’effet de la mesure, seront également abordées. L’exposé présentera les principales applications du calcul quantique en cryptographie, optimisation et calcul scientifique, ainsi que les perspectives offertes par les avancées technologiques récentes dans ce domaine en plein essor. 14h45 - 15h30 : Crises Environnementales et Numérique, Annabelle Collin, Laboratoire de Mathématiques Jean Leray, Nantes Université Dans un contexte marqué par le dérèglement climatique, l’effondrement de la biodiversité et l’épuisement des ressources, il est essentiel d’interroger le rôle du numérique et de mesurer ses impacts. Si ses atouts organisationnels et sociaux sont souvent valorisés, la « dématérialisation » cache en réalité des effets environnementaux majeurs. L’Analyse de Cycle de Vie, en considérant l’ensemble du parcours d’un produit ou d’un usage, met en lumière la complexité et parfois les contradictions de ces impacts, selon les critères retenus et le contexte d’utilisation. Un panorama des conséquences écologiques, sociétales et géopolitiques liées à la généralisation du numérique, sera proposé avant d’ouvrir sur des pistes d’action concrètes. La sobriété numérique apparaît alors comme une voie incontournable dans un monde en crise climatique et aux ressources limitées. 15h30 - 16h30 : Table ronde - Quels sont les besoins des commuanutés scientifiques pour faire face à ces enjeux autour du calcul ? Stéphanie Salmon, Laboratoire de Mathématiques de Reims, Université de Reims |
