CA : Formalisation mathématique

Le but du cours est de fournir une introduction à la formalisation mathématique: il s’agit de la discipline qui s’occupe de rendre définitions et démonstrations mathématiques accessibles à un ordinateur, ce qui permet de les vérifier rigoureusement et d’obtenir en même temps un point de vue nouveau sur les théories qu’on formalise. Pour ce faire, on s’appuie d’une part sur des fondements mathématiques souvent différents de la théorie des ensembles; et, d’autre part, sur des logiciels qui permettent de formaliser les définitions, les énoncés, et les preuves à l’ordinateur. Dans notre cours, on choisira comme fondements la théorie des types dépendants et le calcul des constructions inductives; et on utilisera le logiciel Lean, avec sa bibliothèque Mathlib. Il y aura une alternance de cours théoriques, de cours d’utilisation de Lean, et de travaux pratiques à l’ordinateur.

Ce cours aura lieu de 13h30 à 16h30 aux 3, 5, 10, 17, 19 février, 2, 24, 31 mars, 7 et 14 avril 2026. L’examen est prévu le 10 mars.
Il est nécessaire de venir en cours avec son ordinateur portable.