| Résume | En utilisant l'assistant de preuve Lean, on a récemment
vérifié un résultat très technique de Scholze. Dans une première
partie de l'exposé, j'expliquerai comment fonctionnent les assistants
de preuve et pourquoi ils peuvent être utiles dans la recherche en
mathématiques. Dans une deuxième partie, je rentrerai plus dans les
détails du résultat de Scholze, en expliquant les difficultés qu'on a
rencontré et ce qu'on a appris. Je terminerai en présentant quelques
perspectives pour le futur de la formalisation des maths. |
