BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//LMNO · Laboratoire de mathématiques Nicolas Oresme - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:LMNO · Laboratoire de mathématiques Nicolas Oresme
X-ORIGINAL-URL:https://lmno.unicaen.fr
X-WR-CALDESC:Évènements pour LMNO · Laboratoire de mathématiques Nicolas Oresme
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20250330T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20251026T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20260329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20261025T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20270328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20271031T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260327T140000
DTEND;TZID=Europe/Paris:20260327T150000
DTSTAMP:20260502T163113
CREATED:20260210T171902Z
LAST-MODIFIED:20260311T114109Z
UID:89235-1774620000-1774623600@lmno.unicaen.fr
SUMMARY:Séminaire TNGA : Filippo Nuccio
DESCRIPTION:Orateur : Filippo Nuccio (Université Jean Monnet Saint-Étienne) \n\n\n\nTitre : Expliquer un peu d’arithmétique à un ordinateur \n\n\n\nRésumé : Dans cet exposé j’essaierai d’illustrer ce que signifie formaliser des mathématiques dans un assistant de preuve (j’utiliserai le logiciel Lean)\, en commençant par un exemple simple et par un survol de la pratique de formalisation et des avancées récentes dans ce domaine. Je décrirai ensuite le projet en cours avec de Frutos Fernandez de formalisation de l’arithmétique des corps locaux dans Lean et je conclurai en parlant (au tableau…) d’un résultat obtenu avec Caputo sur la croissance des groupes de classes dans des « fausses Z_p-extensions » de corps de nombres\, et des perspectives à moyen terme de sa formalisation.
URL:https://lmno.unicaen.fr/evenement/seminaire-tnga-filippo-nuccio/
CATEGORIES:Séminaire,Théorie des nombres
END:VEVENT
END:VCALENDAR