L’actualité des dernières semaines est pleine d’annonces tonitruantes que des problèmes mathématiques réputés difficiles ont été résolus par de grandes entreprises de l’IA. Les démonstrations proposées sont très souvent accompagnées d’une « vérification formalisée » à l’aide du logiciel Lean. Cet argument est même régulièrement avancé comme l’assurance définitive qu’un nouveau théorème a été établi.

Dans ces deux exposés, nous ferons le point sur ce qu’est une démonstration formalisée, sur les motivations historiques de cette activité, ainsi que sur les outils théoriques et techniques qui la rendent possible. Nous discuterons ce que formaliser des démonstrations peut apporter aux mathématiques, ainsi qu’aux mathématiciennes et mathématiciens, mais aussi comment cette activité s’articule avec les développements catastrophiques récents de l’interaction entre mathématiques et IA générative.