Seminar Pole Proofs, programs and systems Inria project-team Picube (Inria) Manage talks Formath Day, hour and place Monday at 2:00pm, room 1007 or 3052 The calendar of events (iCal format). In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link. Contact(s) Esaie Bauer Alexis Saurin Next talks Formath Monday April 3, 2023, 2PM, 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 Monday April 17, 2023, 2PM, TBA Arthur Charguéraud (Camus team, ICPS, iCube, INRIA) To be announced. Formath Tuesday May 9, 2023, 0AM, TBA Louise Dubois De Prisque (LSV, CNRS & ENS Paris-Saclay) To be announced. Previous talks Year 2023 Formath Monday March 20, 2023, 3PM, 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é.