Formalization of Mathematics

This is the main repository for Math 681, Formalization of Mathematics, taking place in Fall 2023 at the University of Alberta and the PIMS network. To get started:

1. Install elan, vscode and the Lean4 package for vscode.
2. Clone this repository, and move to the main folder of the repo.
3. Run the commands lake exe cache get and lake build.

Please see the course webpage for additional information and instructions. If you are trying to use this repository to decrypt passwords for recorded lectures, you must first complete the three steps above, and only then run the command to decrypt (otherwise, you will end up compiling for a while).