Séminaire TNGA : Filippo Nuccio

Orateur : Filippo Nuccio (Université Jean Monnet Saint-Étienne)

Titre : Expliquer un peu d’arithmétique à un ordinateur

Résumé : Dans cet exposé j’essaierai d’illustrer ce que signifie formaliser des mathématiques dans un assistant de preuve (j’utiliserai le logiciel Lean), en commençant par un exemple simple et par un survol de la pratique de formalisation et des avancées récentes dans ce domaine. Je décrirai ensuite le projet en cours avec de Frutos Fernandez de formalisation de l’arithmétique des corps locaux dans Lean et je conclurai en parlant (au tableau…) d’un résultat obtenu avec Caputo sur la croissance des groupes de classes dans des « fausses Z_p-extensions » de corps de nombres, et des perspectives à moyen terme de sa formalisation.