Need a roadmap to learn undergrad mathematics through Lean

Stream: new members

[Ao Decipher]

Hi Everyone,

Very very excited to be here. I learned about Lean from a video by Quanta Magazine featuring Prof. @Kevin Buzzard . I got hooked immediately, and totally share the passion.
I'm currently teaching myself undergrad level pure mathematics, and of course I want to master the materials as quickly and thoroughly as possible just like everyone else here, and if I can use Lean to do exercises, that'll be perfect.

I don't know if this question got asked before, but going around in lean community I couldn't find a clear path from beginner to advanced, or from freshman to senior, of getting through all the materials for a standard 4-year undergrad math major.

I know there are a few textbook-like introductions on the community GitHub site, and a list in mathlib, but they are not what I am looking for.
MIT's website has a good example. Here is a piece from their roadmap:

Analysis & Geometry
Tier 1:

- 18.100B Intro to Real Analysis
- 18.700 Linear Algebra/18.701 Algebra I

Tier 2:

- 18.101 Analysis and Manifolds,
- 18.102 Introduction to Functional Analysis,
- 18.103, 18.104, 18.112, 18.152, 18.950, 18.994 ...

Tier 3:

- 18.125 Measure Theory and Analysis,
- 18.155 Differential Analysis I,
- 18.156, 18.952, 18.965, 18.966 ...

I am not studying with an advisor (maybe I should), and a good road map like this is how I make sure I cover all the materials I should. A clear way of integrating Lean into this road map is absolutely necessary for me, so that I don't have to spend too much time wondering which part of mathlib will be a good fit to do exercise with for the books I'm reading.
I know that I'm not a typical math student, but I guess not a lot of math students have advisors who know how to hand pick examples and exercises from mathlib either, so perhaps actually my need is more general than one person?

When I first discovered lean, I was so excited, that I did nothing else but Lean for a week (well, that's a lie, I was also spending quite a bit of time setting up lean.vim or lean.nvim, with help from Julian Berman . But then I realized that I was falling behind on my study schedule, and I have to pause leaning a bit.
I would love to use Lean more if I don't need to slow down my study pace, and I'd love to hear what fellow math students, especially those in ICL (@Kenny Lau, @Chris Hughes , @Ali Sever ... ), have to say about their experience. Any advice will be greatly appreciated.

Thanks a ton!
A.D.

[Kevin Buzzard]

Me and many of the students you mention just learnt Lean from each other and by asking a gazillion questions here on the chat

[Kevin Buzzard]

I gave this course https://xenaproject.wordpress.com/2021/01/24/formalising-mathematics-workshop-1/ which might not be on the community website

[Ao Decipher]

Kevin Buzzard said:

I gave this course https://xenaproject.wordpress.com/2021/01/24/formalising-mathematics-workshop-1/ which might not be on the community website

Thank you for such a quick response! I came across your workshop this morning and I am going to look into it more. It seems to me a great way to learn lean when one already understands the associated math, and I'm seeing if there's a way to do it in the other direction: learn basic lean and then learn "standard" mathematics by reading textbooks and doing corresponding lean exercises. With so many undergrad topics already in mathlib, this should be possible.

I'm also interested in a bit more detail how your students go through their mathematics curriculum, and how heavily is lean involved in their education. Is it a standalone project of fomalising already learned math, or is it a more integrated daily tool, like sage or matlab? If this is documented in your Xena project, I'm sorry I didn't locate it.

[Kevin Buzzard]

This was a course for PhD students who knew the maths already. They had no lean background but by the end of it those who needed grades were able to make mathematical objects and prove theorems about them

[Patrick Massot]

Nobody ever went that far in the direction of teaching using Lean, and it would probably be unwise. You'll get an overview of how people have been using Lean for teaching by watching https://www.youtube.com/watch?v=mTLuON5eRZI&list=PLlF-CfQhukNnO8z3TcFcoKozif9gbl7Yt&index=24

[Kevin Buzzard]

Our course is a traditional maths degree but the students see Lean at the very start because I use it informally in lectures

[Kevin Buzzard]

They then have the option to take an actual "maths in lean" course later on but again I focus mostly on maths they know already

[Kevin Buzzard]

Lean has a big learning curve and to learn maths and lean at the same time seems to be too hard for most people

[Kevin Buzzard]

Patrick also does this -- he goes through maths which the students have just learnt, in lean

[Ao Decipher]

Patrick Massot said:

Nobody ever went that far in the direction of teaching using Lean, and it would probably be unwise. You'll get an overview of how people have been using Lean for teaching by watching https://www.youtube.com/watch?v=mTLuON5eRZI&list=PLlF-CfQhukNnO8z3TcFcoKozif9gbl7Yt&index=24

Very helpful video, will listen through it, thanks!
Why do you think it would be unwise to teach extensively using lean, the reason may already be covered in the video, could you put it in one or two sentences? That would really help me understand how I should use it.

[Ao Decipher]

Kevin Buzzard said:

Lean has a big learning curve and to learn maths and lean at the same time seems to be too hard for most people

OK, so that maybe what Patrick means, unwise to teach Math using Lean...

[Kevin Buzzard]

I started off on this whole Lean thing thinking that it would be a great tool to teach weak undergraduates how to keep their quantifiers in order and to think carefully about the definition of a limit. But all I managed to do was to attract the smart kids who could do that stuff already and were intrigued by the program.

[Ao Decipher]

But if that's the case, that people don't use lean to learn basic stuff, but only on familiar stuff, why would mathematician use lean on things they don't understand yet, i.e. research, dosen't that require them to spend a lot of time setting NEW objects in lean first, which may not exist, because nobody has worked on them yet?

[Kevin Buzzard]

a lot of objects are already in Lean because we have a maths library which is half a million lines of code

[Kevin Buzzard]

and people who are interested in studying X in Lean might build X first, or the things needed to make X

[Ao Decipher]

I'm totally out of my depth now, in your experience, does lean help speed up research compared to pen and paper, or even ipad? I heard Voevodsky saying that 90% of mathematians' time is in checking his proof is correct. In your experience, is that how lean help you and your students save their time in research, by eliminating the need to ensure rigor step by step?

[Sebastien Gouezel]

No, it is much much longer to formalize a proof than to be sure the proof is right. Mathematicians are pretty good at producing correct proofs, and don't need proof assistants for that.

[Johan Commelin]

Currently Lean is not saving us time in research. It might change in the future, and it's one of the reasons why I'm interested in Lean.

[Ao Decipher]

Johan Commelin said:

Currently Lean is not saving us time in research. It might change in the future, and it's one of the reasons why I'm interested in Lean.

That's why i'm interested too!
but does that mean cutting down formalizing time is the most critical in eventually using it for research?
what i'm trying to ask is, let's say 50 years from now, AI isn't able automatically do math research yet, but every mathematician is using a proof assistant, what would be the reason to motivate them to use the assistant?

[Yakov Pechersky]

One of the reasons it is difficult to use mathlib to learn basic math is that a lot of things are hand-waved away in basic math.

[Ao Decipher]

Yakov Pechersky said:

One of the reasons it is difficult to use mathlib to learn basic math is that a lot of things are hand-waved away in basic math.

Haha, that's true. I'm currently working on Real Analysis, using Baby Rudin. A lot of things are pinned down to solid ground, is this a place where using Lean for exercise becoming feasible?

[Kevin Buzzard]

Yes

[Yakov Pechersky]

I said mathlib specifically because mathlib forbids waving things away using sorry. Why does addition and multiplication work the way they do? That's not explained at full rigor at any school education until you get to real analysis. The really nice "proof" of Pythagoras's theorem via the image of triangles and a square is great. But to formalize it rigorously is not something mathlib has done yet. mathlib does not have cycle notation for permutations. mathlib does not have row reduced echelon form for matrices. mathlib doesn't have a rigorous way of writing out the "carry-by-one digit-wise multiplication" that is taught in elementary mathematics. This isn't to say that mathlib shouldn't have these things! But that these elementary results are often either not "rigorous" or are such specializations that mathlib has encoded the general result in a way that might not be accessible.

[Yakov Pechersky]

One could imagine a different maths library in Lean that allows for more of the hand-waving.

[Yakov Pechersky]

Formalizing the exercises in baby Rudin sounds great! I don't think we have a lot on differential forms though, as you get near the end of that book.

[Kevin Buzzard]

The big roadblock for higher differential forms is that we don't have enough API for exterior algebra stuff

[Ao Decipher]

Yakov Pechersky said:

Formalizing the exercises in baby Rudin sounds great! I don't think we have a lot on differential forms though, as you get near the end of that book.

Has anyone worked on formalizing famous textbooks or their exercises? Obviously there will be copyright problems, but building a library of exercise with solutions would greatly help people like me to use Lean for studying.
If no one is doing that, I may try formalizing a few (if the copyright stuff works out), when time allows.
Would this be a valuable contribution?

[Patrick Massot]

Ao Decipher said:

Kevin Buzzard said:

Lean has a big learning curve and to learn maths and lean at the same time seems to be too hard for most people

OK, so that maybe what Patrick means, unwise to teach Math using Lean...

Actually I'm doing a mixture of both. Students have a calculus course during their first term. They see the actual definitions of limits, continuous functions, derivatives (in an elementary context of course), and they see proofs during lectures (up to the intermediate value theorem, mean value theorem, stuff like that). But during exercises sessions they don't have to prove anything, they simply computes limits, derivatives, integrals. Then in my course I cover no new theorem, but they have to actually prove stuff, using epsilons and deltas.

[Patrick Massot]

So it's true that I don't cover any new maths. But the emphasis is exactly the opposite of the emphasis from their previous exposure to these topics.

[Ao Decipher]

Patrick Massot said:

So it's true that I don't cover any new maths. But the emphasis is exactly the opposite of the emphasis from their previous exposure to these topics.

I see, thanks for the details!
Do you think there would be significant benefit from using lean to formalize proofs I've verified the rigor, I mean, if I have already checked the rigor of my proofs (to exercises in baby Rudin) using solution books, would I gain deeping mathematical understanding from typing everything into Lean?

[Kevin Buzzard]

Nobody uses Bourbaki to teach. Bourbaki serves a different purpose, namely to show that mathematics really can be built up rigourously from the axioms. Stuff is sometimes done in a totally different order to the way you would teach it, and sometimes in a far more general way than one would teach it. Books tend not to take that approach. Lean on the other hand does take that approach. Hence formalising a book designed for teaching might not be the right thing to do somehow.

[Johan Commelin]

Kevin Buzzard said:

Nobody uses Bourbaki to teach. Bourbaki serves a different purpose, namely to show that mathematics really can be built up rigourously from the axioms.

And as reference material! Especially the chapters on Lie theory are really great for that.

[Kevin Buzzard]

Yes! That's absolutely a good way to use them. For example it's the only reference I know for the open mapping theorem which works for p-adic Banach spaces and I used this a lot in some of my earlier work

[Sebastien Gouezel]

Do you mean docs#has_strict_fderiv_at.map_nhds_eq_of_surj ?

[Patrick Massot]

Ao Decipher said:

Do you think there would be significant benefit from using lean to formalize proofs I've verified the rigor, I mean, if I have already checked the rigor of my proofs (to exercises in baby Rudin) using solution books, would I gain deeping mathematical understanding from typing everything into Lean?

Did you try the tutorials project? I think that should be a pretty good test.

[Ao Decipher]

Johan Commelin said:

Kevin Buzzard said:

Nobody uses Bourbaki to teach. Bourbaki serves a different purpose, namely to show that mathematics really can be built up rigourously from the axioms.

And as reference material! Especially the chapters on Lie theory are really great for that.

Got it, I also heard Milnor mentioned that he learned topology or something from Bourbaki. Earlier this year, I glimpsed at the first book, and it looked fascinating. I know no one would teach a first math course that way, but I'm always amazed by foundamental building blocks.

[Ao Decipher]

Did you try the tutorials project? I think that should be a pretty good test.

OK I'll try the tutorial project.