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.