Séminaire Pôle Preuves, programmes et systèmes Équipe-projet Inria Picube (Inria) Gestion des séances Séminaire Formath (Formalized Mathematics) Jour, heure et lieu Le lundi à 14h, 1007 ou 3052 Le calendrier des séances (format iCal). Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien. Contact(s) Esaie Bauer Alexis Saurin Le séminaire Formath (Formalized mathematics) est le séminaire de l'équipe Picube. Pour s'abonner à la liste de diffusion, consulter la page https://listes.irif.fr/sympa/info/formath ou écrire aux responsables du séminaire. Prochaines séances Formath Lundi 3 avril 2023, 14 heures, 1007 Olivier Laurent (Équipe Plume, Laboratoire de l'Informatique du Parallélisme (LIP), ENS Lyon) 1, 2, 3, Yalla: Linear Logic in Coq We discuss the formalization of Linear Logic, through the development of the Yalla library for Coq: https://perso.ens-lyon.fr/olivier.laurent/yalla/ The initial specification was to get a library which: would provide standard results on the proof theory of Linear Logic; could be reused, thus in particular able to deal with some variants of the system; should be compatible with the Curry-Howard interpretation of proofs, thus faithful to their computational content. We will describe the evolution of the project and how it matches this specification through the different versions of the library: Yalla 1, Yalla 2 (current version), Yalla 3 (future directions). Following all previous known works, Yalla 1 defined proofs in Prop. It relies on an explicit exchange rule for dealing with the computational content of proofs. Yalla 2 corresponds to a move to Type to be able to extract computational informations from proofs. Yalla 3 will rely on a different way of approaching exchange to be able to deal with local transformations of proofs more easily. Formath Lundi 17 avril 2023, 14 heures, TBA Arthur Charguéraud (Camus team, ICPS, iCube, INRIA) Non encore annoncé. Formath Mardi 9 mai 2023, 0 heures, TBA Louise Dubois De Prisque (LSV, CNRS & ENS Paris-Saclay) Non encore annoncé. Séances passées Année 2023 Formath Lundi 20 mars 2023, 15 heures, 1007 Riccardo Brasca (IMJ-PRG, Université Paris-Cité) Le dernier théorème de Fermat pour les premiers réguliers en Lean Le dernier théorème de Fermat est un résultat en théorie des nombres qui a été conjecturé en 1637, mais qui a été démontré seulement en 1995. La démonstration repose sur des techniques mathématiques modernes et sa formalisation est actuellement hors de portée. Dans cet exposé je vais expliquer la formalisation en Lean d'un cas particulier de ce théorème, où l'on suppose que l'exposant est un nombre premier “régulier” (cette notion sera introduite pendant l'exposé). Je vais aussi décrire l'assistant de preuve Lean et sa bibliothèque mathématique mathlib, et j'expliquerai l'intérêt mathématique d'un tel projet. Aucune connaissance en théorie de nombres est nécessaire pour suivre l'exposé.