Ivan Doubovik (Université de Lille) : Vérification de preuves à l'ordinateur, Lean

Dans cet exposé, je vous parlerai de l'idée derrière la vérification de preuve par ordinateur et à quoi ressemble une preuve formelle. Je vous présenterai Lean, qui est un assistant de preuve, et je vous donnerai quelques exemples élémentaires sur ce dernier. Le point principal de cet exposé est de vous faire connaitre l'existence de tels outils.
Bien qu'il ne s'agisse pas d'un sujet sur lequel je travaille, c'est un sujet qui m'intéresse particulièrement et que j'aimerais explorer après avoir fini ma thèse.