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.


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
Sep 1, 2023 — Dec 31, 2023
Course Number
MATH 681
Section Number
Section Code


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).