https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
An introduction to LEAN https://leanprover.github.io/introduction_to_lean/

Programming in LEAN https://leanprover.github.io/programming_in_lean/#01_Introduction.html

Theorem Proving in LEAN https://leanprover.github.io/theorem_proving_in_lean/

Kevin Buzzard together with Mahammad Pedramfar created a Natural Number game

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/


More advanced material https://leanprover.github.io/

A LEAN proof of the sandwich theorem http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html

For updates:
https://twitter.com/XenaProject

https://xenaproject.wordpress.com/