Comment by aureianimus

All the good resources are listed here: https://lean-lang.org/learn/

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