Formalization of Mathematics
Adam Topaz (University of Alberta)Sep 1, 2023 — Dec 31, 2023
About the course
The last few years have seen amazing advances in interactive proof assistants and their use in mathematics. For example, Lean’s mathematics library mathlib now has over one million lines of code and is still growing in a significant rate. Furthermore, recent highly celebrated successes in the subject, such as the completion of the sphere eversion project and the liquid tensor experiment, suggest that we are approaching a paradigm shift in mathematics, where cutting edge research can be formally verified in a relatively short amount of time. This course will serve as an introduction to the formalization of mathematics, using the Lean4 interactive proof assistant and its mathematics library Mathlib4. See the attached syllabus for an outline of the topics we expect to cover.
Registration
This course is available for registration under the Western Dean's Agreement. To register, you must obtain the approval of the course instructor and you must complete the Western Dean's agreement form , using the details below. The completed form should be signed by your home institution department and school of graduate studies, then returned to the host institution of the course.
Enrollment Details
- Course Name
- Formalization of Mathematics
- Date
- Sep 1, 2023 — Dec 31, 2023
- Course Number
- MATH 681
- Section Number
- A1
- Section Code
Instructor(s)
For help with completing the Western Dean’s agreement form, please contact the graduate student program coordinator at your institution. For more information about the agreement, please see the Western Dean's Agreement website
Other Course Details
Lecture Times
Lectures are Tuesdays and Thursdays, 11am to 12:20pm, Mountain time. All lectures will take place electronically using zoom (or similar software).