Zulip Chat Archive

Stream: general

Topic: Learning resources recommendations?

Cheesehead (Jul 10 2023 at 03:02):

Newbie here. I just started to go through the natural number tutorial, but I found the language is quite different from my installed version (a lean 4 nightly build) of lean. Also, the reference manual belongs to an earlier version, while the theorem proving guide is for lean 4. This made me really struggle to learn. I would like to know if there's any suggestion to get started. Thanks!

Yury G. Kudryashov (Jul 10 2023 at 03:03):

Which webpages do you read?

Cheesehead (Jul 10 2023 at 03:04):

I found these resources in the lean community website: https://leanprover-community.github.io/learn.html

Yury G. Kudryashov (Jul 10 2023 at 03:05):

https://leanprover.github.io/documentation/

Yury G. Kudryashov (Jul 10 2023 at 03:06):

@Kevin Buzzard Is there an "official" version of NNG for Lean 4?

Cheesehead (Jul 10 2023 at 03:14):

It's okay to use an old tutorial, but maybe I need a manual of tactics for lean 4 so that I can switch to the new version.

Yury G. Kudryashov (Jul 10 2023 at 03:28):

You can find some tutorials at https://leanprover.github.io/documentation/

Yury G. Kudryashov (Jul 10 2023 at 03:29):

It looks like doc-gen for Lean 4 doesn't autogenerate a list of tactics.

Cheesehead (Jul 10 2023 at 03:33):

I see, these documentations do help. Thank you.

Kevin Buzzard (Jul 10 2023 at 03:55):

Yury G. Kudryashov said:

Kevin Buzzard Is there an "official" version of NNG for Lean 4?

Jon Eugster put this site https://adam.math.hhu.de/#/g/hhu-adam/NNG4 up and students at Imperial willbe developing it over the summer

Last updated: Dec 20 2023 at 11:08 UTC