BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Discrete Mathematics Group - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://dimag.ibs.re.kr
X-WR-CALDESC:Events for Discrete Mathematics Group
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Asia/Seoul
BEGIN:STANDARD
TZOFFSETFROM:+0900
TZOFFSETTO:+0900
TZNAME:KST
DTSTART:20230101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Asia/Seoul:20240813T163000
DTEND;TZID=Asia/Seoul:20240813T173000
DTSTAMP:20260418T005358
CREATED:20240621T071458Z
LAST-MODIFIED:20240726T000121Z
UID:8784-1723566600-1723570200@dimag.ibs.re.kr
SUMMARY:Peter Nelson\, Formalizing matroid theory in a proof assistant
DESCRIPTION:For the past few years\, I’ve been working on formalizing proofs in matroid theory using the Lean proof assistant. This has led me to many interesting and unexpected places. I’ll talk about what formalization looks like in practice from the perspective of a combinatorialist.
URL:https://dimag.ibs.re.kr/event/2024-08-13/
LOCATION:Room B332\, IBS (기초과학연구원)
CATEGORIES:Discrete Math Seminar
END:VEVENT
END:VCALENDAR