## Stream: new members

### Topic: Getting Started with Lean with prior experience in Coq

#### 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?

#### Johan Commelin (Feb 17 2020 at 06:20):

You'll breeze through the natural number game

#### Johan Commelin (Feb 17 2020 at 06:21):

But it will teach you the system

#### Johan Commelin (Feb 17 2020 at 06:21):

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

#### Johan Commelin (Feb 17 2020 at 06:22):

And the docs/ folder in the mathlib repo

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

#### 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/

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

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

#### Anton Lorenzen (Feb 17 2020 at 09:52):

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

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

#### Rob Lewis (Feb 17 2020 at 10:00):

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

True.

#### Patrick Massot (Feb 17 2020 at 10:03):

I'll add that to my TODO list.

Done.

#### 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