Titre: Preuves formelles : l’informatique au service de la rigueur et de la créativité mathématiques

Resume: Depuis plus d’un demi-siècle, les ordinateurs ont acquis le statut d’instruments de recherche incontournables dans de nombreuses branches de mathématiques fondamentales. Leur puissance de calcul monumentale démultiplie les possibilités d’experimentation et de visualisation, et représente une aide précise pour affiner les conjectures. Mais aussi pour faire des démonstrations. Cet exposé non-technique se propose de discuter le rôle des outils informatiques dans les mathématiques contemporaines, en particulier le potentiel de logiciels appelés prouveurs interactifs, comme Lean ou Coq/Rocq, et de leur bibliothèques de preuves formelles.