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.
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