Best way to learn lean?

Stream: new members

[Martin C. Martin]

Is Learning Lean up to date? I've read through TPiL and even done most of the exercises, but I feel my knowledge is still pretty shaky and I need more practice. I'm a software engineer but studied foundations of math as an undergrad 30+ years ago. I hope to contribute to mathlib, maybe starting with single variable real analysis since I'm familiar with that.

Should I do the tutorials? I vaguely remember hearing of some Lean challenges on a website, was it leetcode? Any other suggestions?

[Matt Diamond]

one thing that I think everyone here agrees upon is that a great way to learn Lean is to just keep proving stuff and asking questions on Zulip when you get stuck

[Heather Macbeth]

Hi, @Martin C. Martin! You can indeed try the #tutorials project, written by @Patrick Massot for students with one semester of university mathematics, or Mathematics in Lean, aimed slightly higher mathematically (maybe most of a university degree in mathematics).

[Matt Diamond]

another thing that I found personally useful was to find interesting lemmas in mathlib and read the source to see how they were proved

[Moritz Doll]

Single variables real analysis is in my opinion a highly nontrivial topic in Lean due to the fact that we try to do everything as abstractly as possible. On the other hand most of the theorems are there already (some versions of l'Hospital and Taylor's theorem are missing). I wonder whether it would make a first good project to write documentation for how to do single variable calculus in mathlib? @Heather Macbeth what are your thoughts on that?

[Moritz Doll]

@Martin C. Martin would you be interesting in doing that?

[Heather Macbeth]

I agree, it's a tricky place to contribute. I'm not sure what to suggest. More documentation doesn't hurt but there is already Section 8.1 of Mathematics in Lean on differential calculus and Section 9.1 on integral calculus.

[Heather Macbeth]

To engage in a bit of self-promotion, one intermediate-level resource for Lean is my tutorial on doing computations efficiently.

[Newell Jensen]

Heather Macbeth said:

To engage in a bit of self-promotion, one intermediate-level resource for Lean is my tutorial on doing computations efficiently.

Haven't looked through the entire tutorial yet but I can say that I am often slowed down in tactic proofs with jumping through the hoops, i.e. massaging, proofs with the algebra steps. Looking forward to seeing if this will help speed that part up for me.

[Heather Macbeth]

@Newell Jensen Looking forward to hearing about your experience!

[Martin C. Martin]

@Matt Diamond I agree that proving stuff is the best way to learn, the question is, what do I prove? I need something that's neither too easy nor too hard. :) Also, your tip about reading lemmas reminds me of how I learned programming in the first place, before I even had a computer at home. From reading the listings in BASIC computer games. Ah the memories.

@Heather Macbeth Starting with tutorials sounds great, and I'll check out Mathematics in Lean, along with your tutorial.

[Newell Jensen]

@Martin C. Martin I have found @Kevin Buzzard 's FM2022 and his videos on YouTube demonstrating the proofs very helpful. I tried the exercises myself and then watched the videos to see how he did the proofs.

[Moritz Doll]

Heather Macbeth said:

I agree, it's a tricky place to contribute. I'm not sure what to suggest. More documentation doesn't hurt but there is already Section 8.1 of Mathematics in Lean on differential calculus and Section 9.1 on integral calculus.

That is true, but it still misses a lot of stuff. I guess my dream would be a Analysis 1 book where all fancy theorems just refer to the mathlib version and the examples are worked out from that. Part of the problem in my opinion with finding things in mathlib for newcomers is that they cannot possibly know the abstractions we use. Who would guess that "Cauchy implies convergent" is in topology/uniform_space - who even knows what a uniform space is.
One good project might be to work out some examples of sequences, i.e., take a book on Analysis 1 and try to do the exercises/examples. My guess is that the most annoying things there are the coercions, finding the theorems, and explicit calculations.

[Bryan Gin-ge Chen]

Heather Macbeth said:

To engage in a bit of self-promotion, one intermediate-level resource for Lean is my tutorial on doing computations efficiently.

(We should add a link to your tutorial to the Learning Lean page! And possibly the linear_combination / polyrith tactic docs as well!)

[Patrick Massot]

Moritz, Mathematics in Lean is meant to answer those questions. But there is still a lot missing.

[Kalle Kytölä]

If there is an update to the Learning Lean page, I think Kevin Buzzard's Formalising Mathematics 2022 course should be added, too. This course is a great resource! One of the things it in my opinion does particularly well is it teaches how to use mathlib in practice (not just Lean). It has become my current recommendation to anyone entering formalization with a bit of math background.

[Matt Diamond]

I agree that proving stuff is the best way to learn, the question is, what do I prove? I need something that's neither too easy nor too hard. :)

@Martin C. Martin True, there's a sweet spot for good practice proofs that can be hard to figure out. As I've been learning Lean, I've tried to think of mathematical objects / statements that are relatively simple but still capture my interest in some way. For example, I figured out how to define Beth cardinals and proved some stuff about them (this was before they were added to mathlib); I also wrote up a proof that sets in Lean are infinite iff they're Dedekind-infinite. Not exactly difficult stuff, but enough to get me reading through the mathlib docs and trying different things.

[Moritz Doll]

Patrick Massot said:

Moritz, Mathematics in Lean is meant to answer those questions. But there is still a lot missing.

Ok, then I change my proposal to "add interesting things to MiL". I was not sure how much PRs that add new content to MiL are wanted

[Arthur Paulino]

I always like to pinpoint that Lean 4 is an amazing programming language as well, not just a theorem prover. And it can teach you strong functional programming fundamentals with a rich type system.

Here's a Python environment manager that I built in Lean 4: https://github.com/arthurpaulino/viper

[Newell Jensen]

Heather Macbeth said:

Newell Jensen Looking forward to hearing about your experience!

Was super excited to see Sage being used. Great tutorial!

[Johan Commelin]

Moritz Doll said:

Patrick Massot said:

Moritz, Mathematics in Lean is meant to answer those questions. But there is still a lot missing.

Ok, then I change my proposal to "add interesting things to MiL". I was not sure how much PRs that add new content to MiL are wanted

I think MiL is currently written by a small number of people with a lot of Lean experience and a very clear vision of what they want to do with this book/project. So it isn't a large-collaborative-project like mathlib. Which is fine, of course.
We just need to lock those people in a room for 2 weeks and fight their universities if they try to put other load on them.

[Pedro Sánchez Terraf]

Heather Macbeth said:

Hi, Martin C. Martin! You can indeed try the #tutorials project, written by Patrick Massot for students with one semester of university mathematics, or Mathematics in Lean, aimed slightly higher mathematically (maybe most of a university degree in mathematics).

Hi! I tried to do leanproject mathematics_in_lean and I got the following error:

Cloning from git@github.com:leanprover-community/mathematics_in_lean.git
info: downloading component 'lean'
error: binary package was not provided for 'linux'
Command '['leanpkg', 'configure']' returned non-zero exit status 1.

Just in case, I tried to bring the tutorials project and that worked just fine. Do you know what might have gone wrong?

[Vincent Beffara]

Or,

def n2 : X -> ℕ
  | (X.None) := 0
  | (X.Single x) := n2 x
  | (X.Many []) := 0
  | (X.Many (x::xs)) := max (n2 x) (n2 (X.Many xs))

(or however this is spelt in Lean4)

[Matt Diamond]

@Vincent Beffara wrong thread?

[Kevin Buzzard]

@Pedro Sánchez Terraf presumably you mean leanproject get mathematics_in_lean. What is the output of elan -V? What operating system are you using?

[Pedro Sánchez Terraf]

Kevin Buzzard said:

Pedro Sánchez Terraf presumably you mean leanproject get mathematics_in_lean. What is the output of elan -V? What operating system are you using?

You're right, that's what I originally entered. elan -V outputs elan 1.4.1 (6a7f30d8e 2022-04-15). I'm running Debian testing.

[Kevin Buzzard]

Try elan self update to see if we can get you up to 1.4.2, and see if that fixes the problem.

[Mauricio Collares]

If elan self update does not work, try installing elan from sid: https://packages.debian.org/sid/elan

[Kevin Buzzard]

It just worked for me on Ubuntu. I think it's only the mac people who have problems with this? but anyway it's great to know that debian sid is up to date!

[Mauricio Collares]

Ah, good! I thought it might depend on whether you installed elan with apt install elan or curl ... | sh, but I can see elan self update installing the newer version locally even if it was installed with apt.

[Pedro Sánchez Terraf]

It worked smoothly! Thank you very much.
... So, the bottom line is (?) that different projects might depend on different versions of elan.

[Mauricio Collares]

No, a single elan is fine for all projects, it's just that all pre-1.4.2 versions of elan are broken (in that they fail to download Lean binaries) due to a GitHub change

[Pedro Sánchez Terraf]

Talking about GitHub, I created a project of my own, for learning (through leanproject new). Am I supposed to treat the folder as a regular git directory? Like, can I do git commit and git push as usual? Or should I use another tool to manage version control?

[Mario Carneiro]

yes, it's a regular git repo

[Thiago Brevidelli Garcia]

Hey peeps, how are you all doing? I recently became interested in formalization (mostly as a pedagogical tool and a way of digesting proofs, I'm not too worried about correctness of existing proofs) and the mathlib project, so I decided to join the chat.

I was wondering: what is the best way for me to learn Lean? I've played the NNG, and I've watched numerous talks on the formalization of different topics, but I feel like I need a helping hand for me to get proficient at Lean. In particular, I'm interested in upcoming (online) workshops and courses on Lean. Any ideas on where I might find those?

Thanks!

[Jireh Loreaux]

IMHO, the best way to learn Lean is by contributing something (doesn't really matter what so long as it doesn't already exist) to mathlib, because then when people review your PRs you learn all the best practices. They'll say "don't do it that way because X, do Y instead," or "check out this golf," or "the tactic X can be used to simplify this."

That being said, at the moment mathlib is in a state of flux because of the port to Lean 4, and so PRs to mathlib3 are being reviewed very slowly, if at all, depending on the content, which is not conducive to learning. So as not to be a buzzkill and to give you some constructive direction to head, I think the next best thing would be working through #mil and/or #tpil, depending on your tastes.

[Jireh Loreaux]

There are these two workshops coming up: https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Two.20workshops, but I think they are geared toward Lean and pedagogy rather than teaching Lean to newcomers. Next year at CIRM there will be a Lean for the Curious Mathematician (LftCM, https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Lean.20for.20the.20Curious.20Mathematician.202024). There may be (read: almost certainly are) other workships I'm missing. Check the #announce stream.

[Floris van Doorn]

Here is a list of upcoming events involving Lean. Some of them involve an online component: https://leanprover-community.github.io/events.html

[Floris van Doorn]

I'm not sure if contributing to mathlib is a great idea if you're very new. It can be quite daunting, since mathlib has high standards for contributed code. However, it is a good idea to choose something small(!) to prove, and while doing it ask questions in this stream when you're stuck. If you manage to finish, post (a link to) your code in this stream to ask for comments and improvements.

[Kevin Buzzard]

For undergraduate mathematicians who want to learn lean I just tell them to choose some mathematical proof they understand and like, and to teach it to lean. Doesn't matter if mathlib knows the theorem already. Make a project with mathlib as a dependency and just go for it

[Thiago Brevidelli Garcia]

Thanks everyone! I think I'll follow Kevin's and Doorn's advice and try to prove something small yet nontrivial (probably Maschke's Theorem for complex representations of finite groups?)!

[Thiago Brevidelli Garcia]

I really hoped I could find a dedicated "teacher" of sorts to help me out at the start, but it looks like there aren't any upcoming online tutorials for a while.

[Jireh Loreaux]

There's plenty of YouTube videos floating around that you can look at for this sort of thing.