BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//jEvents 2.0 for Joomla//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:STANDARD
DTSTART:20221106T010000
RDATE:20230312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20231105T010000
RDATE:20240310T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20241103T010000
RDATE:20250309T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20251102T010000
RDATE:20260308T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20261101T010000
RDATE:20270314T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20271107T010000
RDATE:20280312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20281105T010000
RDATE:20290311T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20221017T153000
RDATE:20221106T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20230312T030000
RDATE:20231105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20240310T030000
RDATE:20241103T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20250309T030000
RDATE:20251102T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20260308T030000
RDATE:20261101T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20270314T030000
RDATE:20271107T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20280312T030000
RDATE:20281105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:50d16c3f8360ecd1ed623a39903c8492
CATEGORIES:Colloquia
CREATED:20231009T100232
SUMMARY: Designing a Formal Hierarchy of Structures
LOCATION:Hill 705
DESCRIPTION:<p>Jeremy Avigad<br aria-hidden="true"> (Department of Philosophy and Depar
 tment of Mathematical Sciences Carnegie Mellon University)</p><p>Title: Des
 igning a Formal Hierarchy of Structures</p><p>Abstract: Over the last few y
 ears, there has been a surge in interest among mathematicians in building d
 igital repositories of formally checked mathematical theorems. Doing so hel
 ps verify the correctness of mathematical results and supports mathematical
  discovery, communication, collaboration, and teaching.<br aria-hidden="tru
 e"> <br aria-hidden="true"> These applications, however, are not the primar
 y motivation for people who work in the field, who care more about the proc
 ess itself and the insights it gives into the inner workings of mathematics
 . In this talk, I will try to convey some of this appeal. Working with math
 ematics' complex network of structures requires substantial expertise, and 
 formalizing mathematics requires making our implicit understanding fully ex
 plicit. I will describe some of the ideas behind the design of the hierarch
 y of structures in Mathlib, the mathematical library of the Lean interactiv
 e proof assistant, and I will reflect on what those ideas tell us about mat
 hematics.</p>
CONTACT:Jeremy Avigad
DTSTAMP:20260827T173349
DTSTART;TZID=America/New_York:20231018T153000
DTEND;TZID=America/New_York:20231018T163000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR