Ask HN: What’s the single best resource for learning Lean (beyond the official docs)?
I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, just to get a feeling.
If you are serious about learning lean, I recommend Functional Programming in Lean for learning it as a programming language and Theorem Proving in Lean for learning it as a proof assistant