What are something to look at for beginners of lean?

Stream: general

[YH]

I have some familiarity of type theory and grad level math, and I just finished the natural_number_game. I want to find something that help me to gain familiarity of syntax of lean, tactics, as well as the mathlib. I was trying to look at the basic localization of commutative ring stuff in lean-scheme but I found I don't know enough of the tactics.

[Kevin Buzzard]

Some more here: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_v1.09beta/

[Kevin Buzzard]

but in practice the way that people learn is that they read TPIL and then start asking questions here.

[Kevin Buzzard]

there are quite a lot of tactics :-/