BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Laboratoire de Mathématiques de Versailles - ECPv6.3.5//NONSGML v1.0//EN CALSCALE:GREGORIAN METHOD:PUBLISH X-ORIGINAL-URL:https://lmv.math.cnrs.fr X-WR-CALDESC:évènements pour Laboratoire de Mathématiques de Versailles 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:20230326T010000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET DTSTART:20231029T010000 END:STANDARD END:VTIMEZONE BEGIN:VEVENT DTSTART;TZID=Europe/Paris:20230207T133000 DTEND;TZID=Europe/Paris:20230207T143000 DTSTAMP:20240328T231844 CREATED:20221028T072446Z LAST-MODIFIED:20230207T151253Z UID:11016-1675776600-1675780200@lmv.math.cnrs.fr SUMMARY:AG : Riccardo Brasca (IMJ-PRG) : Formalisation des mathématiques et l'assistant de preuve Lean DESCRIPTION:Résumé : Je vais parler dans cet exposé de formalisation des mathématiques\, le processus « d’expliquer » des théorèmes à un ordinateur. J’expliquerais comment fonctionnent les assistants de preuve et pourquoi ils peuvent être utiles pour les mathématiciens. Je raconterai aussi l’histoire du\, un projet dont le but était la formalisation d’un résultat très récent de Clausen et Scholze. Je terminerais en montrant en pratique Lean\, un des assistants de preuve le plus utilisé aujourd’hui. Cet exposé n’est pas à propos des fondements des mathématiques\, en particulier aucune connaissance autour de la formalisation est requise. URL:https://lmv.math.cnrs.fr/evenenement/ag-riccardo-brasca-imj-prg/ LOCATION:Bâtiment Fermat\, salle 4205 CATEGORIES:Séminaire AG END:VEVENT END:VCALENDAR