[anatnom]

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.

[0] https://adam.math.hhu.de/#/g/leanprover-community/NNG4

[mcshicks]

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.

https://adam.math.hhu.de/#/g/djvelleman/stg4

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.

https://djvelleman.github.io/HTPIwL/

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.

https://leanprover.zulipchat.com/

[nyssos]

> I am still profoundly confused about what the 'tactics' truly are.

They're macros: a `tactic a` is (after sanding off the implementation details) a function

    tactic_state -> Either (tactic_state, error) (tactic_state, a)

where `tactic_state` is the internal state of the elaborator.