This repository hosts the Lean demos and exercises from the meeting Lean for the Curious Mathematician, held virtually in July 2020. Recordings of the tutorials at this meeting are available on YouTube.
(The repository also hosts the meeting website, but you can ignore this.)
In the src folder, you will find a number of subdirectories containing Lean files:
for_mathlibcontains some background material that you can ignore.demoscontains some files that wre used during the category theory and linear algebra tutorials.exercise_sourcescontains exercises corresponding to each tutorial, organized by day.hintscontains some helpful hints for these exercises.solutionscontains completed exercises, if you're confused and want to peek.
We strongly recommend
installing
Lean with its supporting tool leanproject.
Then you can get this project and open it in VSCode by running:
leanproject get lftcm2020
cp -r lftcm2020/src/exercises_sources/ lftcm2020/src/my_exercises
code lftcm2020
We recommend the second line which copies the exercises to a new directory. Otherwise, if you try to update this project, your exercise solutions could be overwritten or create merge conflicts.
Alternatively, the examples can be executed in browser with the following link:
