A repo for learning Lean through projects

Stream: Lean for teaching

[Juanjo Madrigal]

Hi! :wave:

I've been working on a small Lean repo with projects to get more used to Lean.

Some time ago I started to practice Rust with a platform called CodeCrafters (https://app.codecrafters.io/catalog) that focuses on learning through medium-sized projects divided in many steps. I really like it because each step has a lots of tests and they are small enough to be tackled with little experience but the projects themselves are big enough to learn about maintenability, good practices... all that.

I was wondering if there could be something similar for Lean, so here I have a first trial, https://github.com/juanjomadrigal/lean-crafter .

Right now it only has one project, proving an IMO problem, but I hope to upload more projects in the future.

The system of "checks" is quite primitive; it is also very different to try to check definitions than to try to check propositions or proofs or propositions... but all in all I think it works more or less.

Do you think this "learning by projects" can be useful for people learning Lean?