LeanDojo looks cool! I will check it out. I did the natural number game in lean 3, and was excited to see the author of "How to Prove it" had written an online book, "How to prove it with Lean" to as an accompaniment to the book, but it was written in lean 4. I decided to redo it in Lean 4 (still working on it) and had some troubles but was super happy with the responses I got on the Zulip Chat. It was a bit tricky to install it but the lake system seems like a big improvement over how I installed lean 3. I used the emacs version of lean mode for lean 4.

How to Prove it with lean https://djvelleman.github.io/HTPIwL/ Lean 4 Natural Number Game https://adam.math.hhu.de/#/g/hhu-adam/NNG4 Lean Zulip Chat https://leanprover.zulipchat.com/ Emacs lean 4 mode https://github.com/leanprover/lean4-mode