Get started

1. Install elan, the Lean version manager:

   curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

2. Clone this repository and build it. The first build downloads the Lean version pinned in lean-toolchain:

   git clone https://github.com/ErnestoMFaloh/leanlearn.git leanlearn
   cd leanlearn
   lake build

   The build succeeds with a warning for each sorry in Exercises/. Those are your exercises.
3. Open the folder in VS Code with the Lean 4 extension (leanprover.lean4) and start with module 1.

You need:

• elan: the Lean version manager (see the README).
• Lean 4 and lake (the compiler and the build tool). elan installs the right version automatically the first time you run lake build in this folder.
• VS Code with the Lean 4 extension (leanprover.lean4).

If lean or lake are not found in a new terminal, add this line to your ~/.bashrc (or ~/.zshrc) and open a new terminal:

source ~/.elan/env

How to work

1. Open the project folder in VS Code:

   code leanlearn

2. Open a .lean file. The Lean Infoview panel appears on the right; if it doesn't, press Ctrl+Shift+Enter.
3. Move the cursor through the code. The Infoview shows:
   • the result of each #eval and #check;
   • inside a proof (by ...), the remaining goal.
4. Errors are underlined in red; each sorry is underlined in yellow.
5. To check the whole project from the terminal:

   lake build

How to approach each module

1. Reading: the book chapters listed for the module.
2. Examples: go through the module file, change things and see what happens.
3. Exercises: solve every sorry in the file.
4. Check: run lake exe check <Module> (for example lake exe check Logic). It marks each exercise as ✅ solved, ⏳ pending or ❌ wrong, and says why.
5. Compare: once an exercise is ✅, open the matching file in Solutions/. Different proofs can be equally valid; look for tactics or ideas you didn't use.
6. Wrap-up: commit your work.

When you get stuck

Try for a while first: being stuck is where most of the learning happens. Re-read the examples in the file, check the hints in this guide and look at the goal in the Infoview. If you're still stuck, open the solution, read only the first line or two, and try to finish on your own.

If you keep your solutions in your own fork, commit every time you finish something, even a single exercise:

git add .
git commit -m "Module N: exercise X solved"
git push