BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Journées mathématiques X-UPS
DTSTART:20260416T080000Z
DTEND:20260417T153000Z
DTSTAMP:20260518T091700Z
UID:indico-event-15500@indico.math.cnrs.fr
CONTACT:carole.juppin@polytechnique.edu\;01 69 33 49 59
DESCRIPTION:                               V
 érification formelle de preuves\n                          
                      Journées mathématiques X-UPS 2026\nConf
 érenciers\n\nSébastien Gouëzel\, CNRS - IRMAR (Rennes)\nPatrick Massot\
 , Université Paris-Saclay (Orsay)\nMicaela Mayero\, Université Sorbonne 
 Paris Nord (Villetaneuse)\nBenjamin Werner\, INRIA & École polytechnique 
 (Palaiseau)\n\nOrganisateurs scientifiques\n\nGuillaume Dubach\nPascale Ha
 rinck\nAlain Plagne\nClaude Sabbah\n\nPrésentation du thème\nLes journé
 es X-UPS 2026 auront pour thème la vérification formelle des preuves mat
 hématiques au moyen de logiciels tels que Lean\, Rocq\, Isabelle\, ou HOL
  pour ne citer que les plus connus. Différentes facettes de ce thème ser
 ont abordés par nos orateurs: aspects théoriques (fonctionnement de ces 
 logiciels et fondements mathématiques impliqués\, tels que la théorie d
 es types dépendants utilisée par Lean et Rocq)\, aspects pragmatiques (r
 éflexion sur la place de cet outil dans l'enseignement des mathématiques
  et dans la recherche actuelle) et aspetcts historiques (par exemple la c
 élèbre preuve du théorème des quatre couleurs par George Gonthier et B
 enjamin Werner avec Rocq\, anciennement nommé Coq\, ou plus récemment le
  rôle joué par Lean dans le Liquid Tensor Experiment sous l'impulsion de
  Peter Scholze et Kevin Buzzard). Nos orateurs ont été choisis pour la p
 ertinence et la diversité de leurs expertises avec ces logiciels: Sébast
 ien Gouëzel et Patrick Massot sont des contributeurs actifs de la librair
 e mathlib de Lean\; Benjamin Werner et Micaela Mayero se sont illustrés p
 ar leurs travaux avec le logiciel Rocq. \nPrésentation des journées\nLe
 s journées mathématiques X-UPS sont un stage de formation organisé par 
 le Centre de mathématiques Laurent Schwartz de l'École polytechnique à 
 l'intention des professeurs des classes préparatoires aux grandes écoles
  scientifiques.        Elles se tiennent tous les ans au printemps
 . L'inscription est gratuite mais obligatoire.        L'objectif e
 st double : d'une part satisfaire l'intérêt des professeurs pour l'actua
 lité de la recherche en mathématiques et en informatique\, d'autre part 
 leur apporter des connaissances utilisables dans leur enseignement.   
      Le stage comporte six ou sept conférences éventuellement accom
 pagnées de démonstrations ou de travaux pratiques sur ordinateur. Nous s
 ouhaitons une participation active des stagiaires sous forme de discussion
  et questions aux conférenciers.\nLes Journées mathématiques X-UPS bén
 éficient du soutien de la fondation mathématique Jacques Hadamard (FMJH)
  \n\nhttps://indico.math.cnrs.fr/event/15500/
IMAGE;VALUE=URI:https://indico.math.cnrs.fr/event/15500/logo-3633943427.pn
 g
LOCATION:Amphithéâtre Poisson (École polytechnique)
URL:https://indico.math.cnrs.fr/event/15500/
END:VEVENT
END:VCALENDAR