-
Résumé : Je vais parler dans cet exposé de formalisation des mathématiques, le processus "d'expliquer" des théorèmes à un ordinateur. J'expliquerais comment fonctionnent les assistants de preuve et pourquoi ils peuvent être utiles pour les mathématiciens. Je raconterai aussi l'histoire

