Learning Lean and mathlib

Stream: new members

[Noam Atar]

I am completely new to Lean, and I want to learn it and how to use the mathlib library.
I do have some experience in type theory and proof checking languages (specifically, I have used Agda).
I came from the Natural Numbers game, so I have a feeling about whats going on in Lean, but using the whole library from scratch is pretty daunting to me.
I have read the "first proofs" doc in the mathlib tutorial, but I wouldn't say I could reproduce these proofs without it.
Where can I start? I would prefer a place that builds from (a bit above) zero and has as many exercises as possible.

[Kevin Buzzard]

Theorem Proving In Lean is perhaps a good place for you to start.

[Noam Atar]

I'll try it, thank you.