Dans cet exposé, on fera une brève introduction au logiciel d’assistant de preuve Lean. On parlera de son intérêt comme outil de formalisation et de vérification des mathématiques. On présentera de manière non technique le paradigme de théorie des types sur lequel repose le logiciel, et on illustrera quelques-unes des caractéristiques du logiciel au travers de petites démonstrations interactives en direct. Si le temps le permet, on exposera les grandes lignes d’un projet de formalisation de la version en caractéristique 2 d’un théorème Morel concernant la K-théorie de Witt.
