Check out the "Natural Number Game"[0], which is sort of a practical tutorial but leaves a LOT of things unexplained. I took a few proofs-heavy university classes among the math/cs/philosophy departments so the idea of proving arithmetic from axioms wasn't new, but the NNG still took me an outrageous amount of time (easily 100 hours) and I got nowhere near finishing. Perhaps I just never got things to click into place; I am still profoundly confused about what the 'tactics' truly are.
In my opinion, lean4 is not in any way "for beginners" as you mean it; it is a tool for experts in mathematics.
I absolutely agree that it's not for beginners, but amateurs can still have fun. I did the NNG in lean 3 and again lean 4. It didn't take me 100s of hours but I've also spent a lot of time over the last decade trying to brush up my math skills. One of the main problems with proofs is other than having a mathematician friend who's willing to check its really hard to know if you did it correctly. My son is a mathematician and I still didn't want to ask him to check my proofs! The cool thing for me about lean is I can do some form of math proofs and not have to ask somebody if I got it right.
If you liked that you might like the natural set game as well.
The author of the math book "How to Prove it" Daniel Velleman who I think did the set game also has a "How to Prove it with Lean" which is nice because the exercises correlate to the book.
I've found the lean community on zulip really open to amateurs to want to learn. I asked what I considered a "duh" type of question once I saw the answer, and the guy that helped me is kind of "the lean math" guy.
In my opinion, lean4 is not in any way "for beginners" as you mean it; it is a tool for experts in mathematics.
[0] https://adam.math.hhu.de/#/g/leanprover-community/NNG4