[gtsnexp]

Ask HN: What’s the single best resource for learning Lean (beyond the official docs)?

[mlpoknbji]

Assuming you have some math background but no Lean background: https://adam.math.hhu.de/#/g/leanprover-community/nng4

[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