To begin work on a new problem from the book, create a branch called introX or advancedX (where X should be replaced with the problem number), and create a .lean file with the same name.
Include the following comment block at the top of each new file, below import statements.
/-!
# Intro/Advanced 1 (pp. 1-2) | [IMO ...]
...
## Solution
...
-/