Pourquoi raconter des mathématiques à un ordinateur ?
Patrick Massot
Université Paris-Saclay
https://www.imo.universite-paris-saclay.fr/~patrick.massot/
Date(s) : 25/11/2022 iCal
16h00 - 17h00
De plus en plus de mathématiciens s’amusent en expliquant des mathématiques aux ordinateurs via des logiciels appelés assistants de preuves. Dans cet exposé j’expliquerai à quoi ressemble ce processus, dit de formalisation, quel genre de choses il nous apprend et comment il pourrait même s’avérer utile (en notre sens habituel du mot « utile »).
Patrick MASSOT (Laboratoire de Mathématiques d’Orsay in Université Paris-Saclay)
À titre exceptionnel, l’exposé du colloquium sera précédé d’un TP de découverte des maths formalisées de 10h à 13h dans la salle d’informatique 5-401 (Bâtiment 5 (grand bâtiment), escalier 2, étage 4, bloc A) à St Charles.
Emplacement
Saint-Charles - FRUMAM (2ème étage)
Catégories