Orateur
Description
Les assistants de preuve sont des langages dans lesquels on explique à un ordinateur des preuves mathématiques,
l'ordinateur se chargeant de vérifier que le passage d'une ligne à la suivante respecte toujours les règles de la logique. Cela permet
entre autres avantages de garantir quasiment à 100% la correction des démonstrations.
Je présenterai l'assistant de preuves Lean et sa bibliothèque de mathématiques formalisées Mathlib, avec un point de vue de mathématicien praticien
(et donc sans parler du tout du fonctionnement interne des assistants de preuve) :
quelles différences de point de vue faut-il avoir quand on démontre un résultat sur papier ou quand on le formalise, quels sont les types d'arguments les plus
difficiles de chaque côté, quels sont les écueils à éviter, etc.
Je m'appuierai principalement sur des exemples concrets. Je démontrerai puis expliquerai la formalisation d'un théorème sur les vecteurs de translation asymptotique de fonctions 1-lipschitziennes.
Ensuite, je me concentrerai sur la notion de fonction $C^n$, telle qu'exposée dans les livres ou dans les cours, puis telle que formalisée dans Mathlib -- il y a des différences significatives entre les deux,
qui illustrent bien les particularités des mathématiques formalisées.