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:Jeremy Avigad (Department of Philosophy and Department of Mathematical Scie
 nces Carnegie Mellon University)\nTitle: Designing a Formal Hierarchy of St
 ructures\nAbstract: Over the last few years, there has been a surge in inte
 rest among mathematicians in building digital repositories of formally chec
 ked mathematical theorems. Doing so helps verify the correctness of mathema
 tical results and supports mathematical discovery, communication, collabora
 tion, and teaching.  These applications, however, are not the primary motiv
 ation for people who work in the field, who care more about the process its
 elf and the insights it gives into the inner workings of mathematics. In th
 is talk, I will try to convey some of this appeal. Working with mathematics
 ' complex network of structures requires substantial expertise, and formali
 zing mathematics requires making our implicit understanding fully explicit.
  I will describe some of the ideas behind the design of the hierarchy of st
 ructures in Mathlib, the mathematical library of the Lean interactive proof
  assistant, and I will reflect on what those ideas tell us about mathematic
 s.\n
X-ALT-DESC;FMTTYPE=text/html:<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:20260827T183405
DTSTART;TZID=America/New_York:20231018T153000
DTEND;TZID=America/New_York:20231018T163000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR