Séminaire en ligne, 11 mars 2021

Pour assister à la rencontre, se rendre sur https://ent-services.ens-lyon.fr/entVisio/ choisir Chocola dans le menu déroulant, mettre son nom comme identifiant, et Bruxelles sans majuscule comme dernier champ. Autoriser les popups, et changer de navigateur au besoin.

10h: accueil et problèmes de connexion 10h15: début de l'exposé 11h15: questions et discussion 12h: adieu et problèmes de déconnexion Merci aux auditeurs de couper micro et caméra (sauf éventuellement, lorsqu'ils souhaitent poser une question). Les questions peuvent aussi être posées dans la fenêtre de chat.

En cas de problème ou de question, écrire à chocola-gestion chez ens-lyon.fr.

Programme

10:00 – 12:00: Assia Mahboubi (Inria Gallinette, Nantes)

Invited talk: Machine-Checked Computer-Aided Mathematics

This talk presents an overview of three contributions to the formal verification of mathematics in dependent type theory. The first of these contributions deals with the realization of a library of digitized mathematics, covering the standard undergraduate background in algebra as well as some more advanced chapters in finite group theory. The two other contributions are related to the issues pertaining to the formal verification of computational mathematical proofs, by the means of symbolic algorithms and of rigorous numerical methods respectively. We conclude with a few perspectives on the formal verification of computer-aided mathematics.