MTH1001 in Lean

These are Lean-based lecture notes for the University of Exeter module MTH1001 (Mathematical Structures).

These notes depend on Lean, VS Code, and mathlib. You can install them following the instructions in the mathlib repository, https://github.com/leanprover-community/mathlib.

To use this tutorial, you need to set up a project folder. Open a terminal and type:

leanproject get https://github.com/gihanmarasingha/mth1001_sphinx

Then open the project in VS Code:

code mth1001_sphinx

Once VS Code starts, open the file welcome.lean. That will load the notes in a separate window, and you are good to go.

Acknowledgements

This document is based on Mathematics in Lean, by Jeremy Avigad et al.