Zulip Chat Archive

Stream: new members

Topic: Getting Started with Lean with prior experience in Coq


view this post on Zulip Donald Sebastian Leung (Feb 17 2020 at 06:19):

As a computer science undergraduate with close to 1 year of experience with Coq who would like to get started with Lean for doing "fashionable mathematics" (as Kevin Buzzard puts it) at the undergraduate level, what tutorial would you recommend?

view this post on Zulip Johan Commelin (Feb 17 2020 at 06:20):

You'll breeze through the natural number game

view this post on Zulip Johan Commelin (Feb 17 2020 at 06:21):

But it will teach you the system

view this post on Zulip Johan Commelin (Feb 17 2020 at 06:21):

Then there's the book "Theorem proving in Lean"

view this post on Zulip Johan Commelin (Feb 17 2020 at 06:22):

And the docs/ folder in the mathlib repo

view this post on Zulip Johan Commelin (Feb 17 2020 at 06:22):

And finally, just pick a topic you like, and start working on it. Make sure to show your files here and ask for feedback.

view this post on Zulip Bryan Gin-ge Chen (Feb 17 2020 at 06:29):

There's also the lecture notes to the course Logical Verification in Lean: https://lean-forward.github.io/logical-verification/2019/

view this post on Zulip Donald Sebastian Leung (Feb 17 2020 at 08:50):

Thanks for your recommendations :+1: Since I've done the natural number game before, Theorem Proving in Lean sounds like a good next step.

view this post on Zulip Anton Lorenzen (Feb 17 2020 at 09:51):

Especially the mathlib/docs/extras is really useful. I think it is what took me from "knows how to fill in a sorry" to "can deal with most problems themselves".

view this post on Zulip Anton Lorenzen (Feb 17 2020 at 09:52):

And https://leanprover.github.io/reference/tactics.html is a nice encyclopedia of builtin tactics

view this post on Zulip Patrick Massot (Feb 17 2020 at 09:54):

You can also clone the tutorial project or use its only file so far online if you are patient enough.

view this post on Zulip Rob Lewis (Feb 17 2020 at 10:00):

Oh, we should bump the Lean/mathlib version on the tutorial.

view this post on Zulip Patrick Massot (Feb 17 2020 at 10:01):

True.

view this post on Zulip Patrick Massot (Feb 17 2020 at 10:03):

I'll add that to my TODO list.

view this post on Zulip Patrick Massot (Feb 17 2020 at 13:47):

Done.

view this post on Zulip Jasmin Blanchette (Apr 03 2020 at 12:50):

New link for the lecture notes mentioned by Bryan: https://lean-forward.github.io/logical-verification/2020/index.html#material


Last updated: May 13 2021 at 21:12 UTC