Learning roadmap

Stream: general

[Ignat Insarov]

How should I go about learning Lean? I am already more or less familiar with Coq and some other programming languages. My aim is to formally verify some common stuff from Mathematics and Computer Science, first for education, then for work. Nothing too fancy. Are there some books or courses that I should look into?

[Alex J. Best]

Have you checked out https://leanprover-community.github.io/learn.html ? If you already have some experience with coq maybe just looking through #tpil will be a good way to go to see the syntax explained.

[Ignat Insarov]

I overlooked it. Is it linked from <https://leanprover.github.io/links/>? Cannot spot. Looks like exactly what I need.

[Kevin Buzzard]

No -- leanprover.github.io is Microsoft -- the community website is much more helpful for beginners.

[Kevin Buzzard]

MS are busy working with Lean 4, which is not yet ready for most mathematics, and they abandoned Lean 3 long ago; the community fork of Lean 3 is maintained by the community and their website contains a huge list of resources.

[Ignat Insarov]

I see, thanks. So building Lean 4 clone from Git was a misstep.

[Patrick Massot]

There is a link from https://leanprover.github.io/documentation/ but it's still no so easy to identify as the main link to follow.

[Bryan Gin-ge Chen]

I suppose we could submit a PR adding the community site to this page: https://github.com/leanprover/leanprover.github.io/blob/master/links/index.md

I'm not sure which section it would belong under though.