Conférence de S. Gouëzel

Assistants de preuve et Peter Scholze

Motivé par un manque de confiance en une de ses propres preuves, Peter Scholze (médaille Fields 2018) 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.