This is Lean 3 code; Lean 3 is now end-of-life. A Lean 4 version of this course is available here
Repository for the Jan-Mar 2021 EPSRC TCC course on formalising mathematics, delivered to mathematicians at Imperial, Oxford, Bristol, Bath and Warwick.
In this course, we're going to be turning maths theorems into levels of a computer game called Lean. We'll start off with proving basic stuff like composite of injective functions is injective. We'll move on to harder mathematics as the course goes on. The course comprises 8 workshops. You don't have to do all the questions in each workshop.
I took the slightly unconventional approach of blogging about each workshop rather than writing a formal document. Here are links to the eight workshop blog posts (plus an introductory post which explains my motivations for teaching the course):
- Introduction
- Logic, sets, functions, relations
- Groups and subgroups
- Sequences and limits
- Topology
- Filters
- Limits
- Quotients
- Group cohomology
You should know some mathematics. For example if you're a second year undergraduate you should easily be able to be able to solve the levels from first few weeks.
You should also get Lean 3 and the community tools installed on your computer. This is unfortunately not as simple as it could be. Here are the instructions . It's recommended that you follow them to the letter.
Assuming you have Lean and the user tools installed, first install the repository by firing up a command line, navigating to the directory you want to install this project in, and then typing
leanproject get ImperialCollegeLondon/formalising-mathematics
code formalising-mathematics
and then open up some of the files in src/week1 and you're up and running. Look at the README.md file in src/week1 for more instructions. Fill in the sorrys. Try a couple of levels of the natural number game if you're not sure what's going on.
Important note: if you just use git clone or some "download zip file" option on github then it won't work; you will not have access to Lean's maths library if you try this way (so imports won't work etc).
Well, you can always play along using the community web editor. Here are the four worlds for week 1. You might have to wait for a minute or so until "Lean is busy..." becomes "Lean is ready!". Also, feel free to ask for assistance on the Lean Zulip chat (login required, real names preferred, be nice).