Hi! Best way(s) to get stuck in?

Stream: new members

[Avery]

Hello! I'm Avery, I'm a PhD student (albeit in a mostly unrelated field)/CS grad but I'm here because I find the whole formalising concept fascinating; I suppose for me this is more of an academic hobby interest rather than trying to further my work? Regardless, I've worked through the natural numbers game and wasn't sure if there was a recommended path(s) to get more comfortable with lean? I've seen the Theorem Proving With Lean book thrown about, and similarly a tutorial github repo?
For instance, I considered working through basic mathematics ala the natural numbers game but I wasn't sure how much of a use of my own time (I know it'd be useless when mathlib exists!) it'd be. Mostly my aim at this point is satisfying my own curiosity but if at some point I'm able to contribute anything at all to mathlib I'd love to :)

I hope this isn't too much of a vague ramble! Cheers :)
tl;dr is there a recommended path to get comfortable w/Lean after trying out the naturals game?

[Patrick Massot]

Welcome! Our community answer to this is at https://leanprover-community.github.io/learn.html

[Avery]

ah, excellent - figured there would be a collated resource I was missing :D thanks!