Assistants de preuve et Peter Scholze

Motivé par un manque de confiance en une de ses propres preuves, Scholze a demandé à la communauté des preuves formalisées sur ordinateur s'il était possible de vérifier formellement cette preuve. Je raconterai comment cela a été fait avec l'assistant de preuves Lean et sa bibliothèque Mathlib de mathématiques formalisées dont je suis l'un des gestionnaires. Ce sera l'occasion de parler plus généralement d'assistants de preuves, ce qu'ils permettent, et leurs limitations.