Cours spécialisé ()
Contact : riccardo.brasca à imj-prg.fr
Notes de cours : https://riccardobrasca.github.io/teaching/
L'objectif principal de ce cours est d'introduire Lean et de familiariser les étudiant.e.s avec la formalisation de mathématiques dans un assistant de preuve. Lean est l'un des theorem provers, c'est-à-dire un logiciel permettant de coder des objets mathématiques, d'énoncer des théorèmes et de vérifier formellement la correction de leurs preuves. Le cours donnera aux étudiant.e.s une première expérience concrète de la formalisation mathématique : prise en main du langage, manipulation des preuves interactives, usage d'une bibliothèque mathématique existante, et écriture de développements formels simples puis plus structurés. Il comportera également une introduction à la théorie des types sur laquelle repose Lean, afin de donner aux étudiant.e.s un aperçu des fondements logiques et informatiques du système. Une partie du cours sera consacrée à l'étude de thèmes mathématiques choisis en fonction des intérêts du groupe. On pourra par exemple travailler sur des thèmes plus avancés, issus notamment de la théorie des nombres, de la topologie générale, de l'algèbre commutative ou de la géométrie algébrique, selon les intérêts du public et les possibilités offertes par la bibliothèque mathématique disponible. Au-delà de l’aspect technique, le cours vise aussi à présenter la formalisation comme un domaine mathématique à part entière, à l’interface entre logique, informatique et pratique contemporaine des mathématiques. Une attention pourra également être portée aux liens récents entre formalisation et intelligence artificielle, par exemple autour de l'autoformalisation, de l'assistance à la preuve par modèles de langage, ou plus généralement des interactions entre outils de preuve formelle et méthodes d'apprentissage automatique.
Parmi les réalisations récentes figurent notamment la formalisation du cœur technique des Lectures on Analytic Geometry de Clausen–Scholze, ou encore la formalisation d'un théorème généralisé de Carleson, un résultat central d'analyse harmonique, en Lean.