Getting Started with Lean with prior experience in Coq

Stream: new members

[Donald Sebastian Leung]

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?

[Johan Commelin]

You'll breeze through the natural number game

[Johan Commelin]

But it will teach you the system

[Johan Commelin]

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

[Johan Commelin]

And the docs/ folder in the mathlib repo

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

[Donald Sebastian Leung]

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

[Anton Lorenzen]

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".

[Anton Lorenzen]

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

[Patrick Massot]

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

[Rob Lewis]

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

[Patrick Massot]

True.

[Patrick Massot]

I'll add that to my TODO list.

[Patrick Massot]

Done.

[Jasmin Blanchette]

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