Zulip Chat Archive

Stream: general

Topic: Learning roadmap

Ignat Insarov (Oct 03 2021 at 18:11):

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 (Oct 03 2021 at 18:16):

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 (Oct 03 2021 at 18:18):

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

Kevin Buzzard (Oct 03 2021 at 18:19):

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

Kevin Buzzard (Oct 03 2021 at 18:20):

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 (Oct 03 2021 at 18:26):

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

Patrick Massot (Oct 03 2021 at 18:56):

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 (Oct 03 2021 at 19:02):

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.

Last updated: Dec 20 2023 at 11:08 UTC