# Zulip Chat Archive

## Stream: new members

### Topic: Best way to learn lean?

#### Martin C. Martin (Sep 22 2022 at 16:12):

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 (Sep 22 2022 at 16:56):

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 (Sep 22 2022 at 16:57):

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 (Sep 22 2022 at 16:58):

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 (Sep 22 2022 at 17:20):

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 (Sep 22 2022 at 17:23):

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

#### Heather Macbeth (Sep 22 2022 at 17:23):

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 (Sep 22 2022 at 17:28):

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

#### Newell Jensen (Sep 22 2022 at 17:36):

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 (Sep 22 2022 at 17:44):

@Newell Jensen Looking forward to hearing about your experience!

#### Martin C. Martin (Sep 22 2022 at 17:49):

@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 (Sep 22 2022 at 17:52):

@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 (Sep 22 2022 at 18:30):

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 (Sep 22 2022 at 18:49):

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 (Sep 22 2022 at 20:05):

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

#### Kalle Kytölä (Sep 22 2022 at 20:14):

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 (Sep 22 2022 at 21:01):

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 (Sep 22 2022 at 22:05):

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 (Sep 22 2022 at 23:53):

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 (Sep 23 2022 at 00:10):

Heather Macbeth said:

Newell Jensen Looking forward to hearing about your experience!

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

#### Johan Commelin (Sep 23 2022 at 05:23):

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 (Sep 27 2022 at 14:41):

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 (Sep 27 2022 at 14:58):

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 (Sep 27 2022 at 15:29):

@Vincent Beffara wrong thread?

#### Kevin Buzzard (Sep 27 2022 at 18:22):

@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 (Sep 27 2022 at 18:36):

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 (Sep 27 2022 at 18:40):

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 (Sep 27 2022 at 18:40):

If `elan self update`

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

#### Kevin Buzzard (Sep 27 2022 at 18:41):

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 (Sep 27 2022 at 18:43):

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 (Sep 27 2022 at 18:45):

It worked smoothly! Thank you very much.

... So, the bottom line is (?) that different projects might depend on different versions of `elan`

.

#### Mauricio Collares (Sep 27 2022 at 18:45):

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 (Sep 27 2022 at 18:49):

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 (Sep 27 2022 at 19:11):

yes, it's a regular git repo

#### Thiago Brevidelli Garcia (Mar 09 2023 at 22:41):

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 (Mar 09 2023 at 23:04):

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 (Mar 09 2023 at 23:06):

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 (Mar 09 2023 at 23:11):

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 (Mar 09 2023 at 23:15):

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 (Mar 10 2023 at 00:21):

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 (Mar 10 2023 at 21:36):

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 (Mar 10 2023 at 21:38):

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 (Mar 10 2023 at 22:23):

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

Last updated: Dec 20 2023 at 11:08 UTC