Séminaires : Séminaire Groupes Réductifs et Formes Automorphes

Equipe(s) : fa, tn,
Responsables :Alexis Bouthier, Cong Xue
Email des responsables : alexis.bouthier@imj-prg.fr, cong.xue@imj-prg.fr
Salle :
Adresse :
Description

Orateur(s) Riccardo BRASCA - IMJ,
Titre Comment expliquer un théorème de Scholze à un ordinateur
Date10/01/2022
Horaire10:30 à 12:00
Diffusion
RésumeEn 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.
Salle1013
AdresseSophie Germain
© IMJ-PRG