tutorial for mathlib

Stream: new members

[Robert Watson]

Hi there, I've done the Natural Numbers Game (fun and mostly straight forward), understand or have done the Tutorials, and read quite a lot of Theorem_Proving_In_Lean to the extent I felt was required to understand the preceding better and to get a better overview of Lean. Also I started using Lean 4 but gave up, now using Lean 3, due to better docs and seemingly easier to use/install and more stable toolchain. So far so good. However, the moment I try to understand what is going on in Mathlib outside of the range of tactics I've already been taught, I am at a complete loss. What is the next step if I want to, say, do linear algebra in Lean?

[Sebastien Gouezel]

You could have a look at https://github.com/leanprover-community/lftcm2020, which contains tutorials and introductions to various parts of mathlib.

[Robert Watson]

OK. Thanks.

[Kevin Buzzard]

@Robert Watson I did some vector space stuff two weeks ago in the course I'm teaching right now : see e.g. https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/tree/master/src/section10vectorspaces

[Robert Watson]

I just wanted to give you guys some positive feedback: the lftcm2020 series is so far exactly what I needed to get over the hurdle of going from simply having done some examples in the Natural Numbers Game and the Tutorials to understanding how to use tactics outside of those sandboxes. Thanks.