More lean programming tutorial

[wiio12]

Great work here! However, I struggle to find more lean 3 programming tutorials, including documentation of lean library. Where can I find these tutorials?

[fzyzcjy]

Hi, I am also looking for material learning lean as FP language. Did you find something?

[oxarbitrage]

I will share my little experience if that can help someone.

This 2 resources are pretty good:

http://leanprover.github.io/logic_and_proof/
https://cs.brown.edu/courses/cs1951x/static_files/main.pdf

Then the book for lean 4 seems to be good, however i didn't tried lean4 yet:

https://leanprover.github.io/theorem_proving_in_lean4/

The lean community chat is good for specific questions like if you get stuck trying to do something. https://leanprover.zulipchat.com/

Mathlib is hard even if you know the mathematics, it is easier to start a personal project than trying to make contributions into mathlib. I started a little personal project for learning purposes but i make a lot if mistakes as i am learning functional programming at the same time as lean.

https://github.com/oxarbitrage/salsa20

What i think i will do now is try to learn more haskell and functional programming hoping that will make lean a little easier for me.

Another thing i did is checking other projects written in lean, there are quite a few.