See also Terence Tao's blog posts detailing how he's using Lean 4:

https://terrytao.wordpress.com/tag/lean4/

Assuming I did proofs in highschool algebra and geometry courses, is there any tutorial that would make lean4 accessible? I think computer assisted theorem proving could be great educationally, but this post would be complete gobligook to most students despite the title.

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

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/

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

I enjoyed working through "Theorem Proving in Lean 4", although it doesn't go deep into the mathematics side of things. I intend to work through "Mathematics in Lean"[2] to get more detail on that, but I want to finish "Programming Language Foundations in Agda" first.

[1]: https://lean-lang.org/theorem_proving_in_lean4/

[2]: https://github.com/leanprover-community/mathematics_in_lean

Edit: Oh, also the "Natural Number Game" is a nice, short intro to the theorem proving that gets straight to the point: https://adam.math.hhu.de/

This game is a decent introduction, though I think it has plenty of room for improvement: https://adam.math.hhu.de/#/g/leanprover-community/nng4.

Maybe try “Programming Language Foundations in Agda” instead.

https://plfa.github.io

I think you should probably understand formal logic, and may proof theory and also abstract algebra as a pre-req.

To the author, Lean is not mathlib (A fact that you will probably get sick of hearing if you spend time in the zulip). If your objective with lean is to use mathlib, you should try following the mathlib tutorial as well.

This is about the worst written "beginner's companion". Not sure what the purpose is here.