AG : Riccardo Brasca (IMJ-PRG) : Formalisation des mathématiques et l’assistant de preuve Lean

Chargement Évènements

« Tous les Évènements

AG : Riccardo Brasca (IMJ-PRG) : Formalisation des mathématiques et l’assistant de preuve Lean

7 février / 13:30 - 14:30

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.

AG : Riccardo Brasca (IMJ-PRG) : Formalisation des mathématiques et l’assistant de preuve Lean

Détails

Date:
7 février
Heure :
13:30 - 14:30
Catégorie d’Évènement:

Lieu

Bâtiment Fermat, salle 4205

Organisateurs

Pierre-Guy Plamondon
Thomas Lanard