Dans cet exposé nous aborderons deux sujets: la théorie de la stabilisation et l'IA pour les mathématiques. La stabilisation est une branche de la théorie du contrôle qui consiste à se demander: "si je peux agir sur un système, que puis-je lui faire faire ?" Cette théorie a la particularité de mêler des aspects très théoriques et très divers ainsi que des aspects très appliqués. Nous parlerons ensuite d'IA pour les mathématiques et nous nous demanderons s'il est possible d'apprendre des mathématiques à une IA. En particulier, est-ce qu'une IA […]

Les « assistants de preuve » sont des logiciels qui permettent d'entrer un énoncé de théorème et sa démonstration comme un programme, la compilation dudit programme garantissant que la démonstration proposée prouve effectivement l'énoncé donné. Initiés dans les années 60, ils font l'objet d'une grande activité scientifique depuis une trentaine d'années et ont permis de vérifier la correction d'énoncés tout à fait non triviaux. Intéressé par ces développements, je me suis appliqué à démontrer la simplicité du groupe alterné au sein du logiciel Lean et de sa librairie mathématique mathlib. […]

Il y a 266 ans, Euler introduit la première description mathématique cohérente des fluides et 25 ans plus tard, Monge initie la théorie du transport optimal. Ces sujets n'ont rien perdu de leur actualité et je voudrais expliquer leur lien via l'optimisation combinatoire.