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 du, un projet dont le but était la formalisation d’un résultat très récent de Clausen et Scholze. Je terminerais en montrant en pratique Lean, un des assistants de preuve le plus utilisé aujourd’hui. Cet exposé n’est pas à propos des fondements des mathématiques, en particulier aucune connaissance autour de la formalisation est requise.