"Je vais parler dans cet exposé de formalisation des mathématiques, le processus ""d'expliquer"" des théorèmes à un ordinateur. J'expliquerai comment fonctionnent les assistants de preuve et pourquoi ils peuvent être utiles pour les mathématiciens. Je raconterai aussi l'histoire d'un projet dont le but était la formalisation d'un résultat très récent de Clausen et Scholze. Je terminerai en montrant en pratique Lean, un des assistants de preuve les plus utilisés aujourd'hui. Cet exposé n'est pas à propos des fondements des mathématiques, en particulier aucune connaissance autour de la formalisation est requise. "