If you see this on GitHub, you are probably looking for the
official website
or its source code which is in the docs folder.
If you downloaded this using leanproject then you probably want to
open this folder in VSCode and start doing the exercises.
For instance, on Tuesday morning, you can do inside this root folder
git pull
cp src/exercises_sources/tuesday/morning.lean src/tuesday_morning.lean
code .
And then click on src/tuesday_morning.lean in the VSCode file explorer
to start playing. The reason we don't recommend you edit our source file
directly is your modifications would get overwritten when you'll update
the repository using git pull.