Seminars & Colloquia Calendar

Download as iCal file


Designing a Formal Hierarchy of Structures

Jeremy Avigad

Location:  Hill 705
Date & time: Wednesday, 18 October 2023 at 3:30PM - 4:30PM

Jeremy Avigad (Department of Philosophy and Department of Mathematical Sciences Carnegie Mellon University)

Title: Designing a Formal Hierarchy of Structures

Abstract: Over the last few years, there has been a surge in interest among mathematicians in building digital repositories of formally checked mathematical theorems. Doing so helps verify the correctness of mathematical results and supports mathematical discovery, communication, collaboration, and teaching. These applications, however, are not the primary motivation for people who work in the field, who care more about the process 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 mathematics' complex network of structures requires substantial expertise, and formalizing mathematics requires making our implicit understanding fully explicit. I will describe some of the ideas behind the design of the hierarchy of structures in Mathlib, the mathematical library of the Lean interactive proof assistant, and I will reflect on what those ideas tell us about mathematics.

Special Note to All Travelers

Directions: map and driving directions. If you need information on public transportation, you may want to check the New Jersey Transit page.

Unfortunately, cancellations do occur from time to time. Feel free to call our department: 848-445-6969 before embarking on your journey. Thank you.