Ensimag, Amphi E
8 February 2024 - 14h00
Formalisation d'un objet geometrique dans l'assistant de preuve Lean: le cas des grassmanniennes.
by Sophie Morel from CNRS - ENS-Lyon
Résumé : Lean (https://lean-lang.org) est un logiciel pour formaliser et vérifier des théories mathématiques. L'exposé s'adressera à des néophytes de Lean et des assistants de preuve. Si r est un entier positif et V est un espace vectoriel (par exemple $mathbb{R}^n$), la r-grassmannienne de V est l'ensemble des sous-espaces de dimension r de V, qu'on peut aussi voir comme un quotient de l'ensemble des familles libres à r éléments de V. En particulier, si r = 1, on obtient l'espace projectif de V.
Je commencerai par montrer la formalisation de ces objets en Lean. J'expliquerai ensuite la définition d'une variété différentielle (un espace qui ressemble localement à une boule ouverte d'un espace $mathbb{R}^n$), et leur formalisation en Lean. Enfin, je discuterai la structure naturelle de variété différentielle sur les grassmanniennes, en me concentrant sur les cas où r = 1 ou 2 et où l'espace V est $mathbb{R}^n$, et je parlerai de quelques difficultés que l'on rencontre lorsque l'on essaie de formaliser cette construction en Lean.
Courte biographie: Sophie Morel est une mathématicienne internationalement reconnue pour ses travaux en géométrie algébrique, théorie des représentations et théorie des nombres. En 2009, à tout juste 30 ans, elle a été la première femme professeur en mathématique à l'université de Harvard. Elle a été membre d'autres prestigieux établissements universitaires aux États-Unis. Elle est maintenant directrice de recherche au CNRS et à l'ENS-Lyon. https://en.wikipedia.org/wiki/Sophie_Morel
Séminaire retransmis en visio sur https://univ-grenoble-alpes-fr.zoom.us/j/91984060230?pwd=ZHV2cm91dzBITjJrU1JQR241TjVvZz09
