learn maths with lean

Stream: general

[Matthew Pocock]

Is there a "learn maths using lean" resource I can work through? I guess I'm looking for an undergrad-level course where the exercises are in lean or could be implemented in lean. I am happy to help with copyediting or content feedback if there's something in progress but not ready for public consumption.

[Kevin Buzzard]

Is "Mathematics in Lean" https://leanprover-community.github.io/mathematics_in_lean/ what you're looking for? Alternatively there is my undergraduate course (still in Lean 3 though, although I'll be translating it in December so it can run in Lean 4 in Jan) and Heather's course "the mechanics of proof" https://hrmacbeth.github.io/math2001/ is also in Lean 4.

[Matthew Pocock]

Kevin Buzzard said:

Is "Mathematics in Lean" https://leanprover-community.github.io/mathematics_in_lean/ what you're looking for?

I really need to work through this, but from skimming through it, it seemed to assume you already knew all the maths, and the focus was on doing that maths with lean4.

Alternatively there is my undergraduate course (still in Lean 3 though, although I'll be translating it in December so it can run in Lean 4 in Jan) and Heather's course "the mechanics of proof" https://hrmacbeth.github.io/math2001/ is also in Lean 4.

Thanks. I guess I'm looking for something more like "math 101 - equations, limits, calculus, oh my!" where incidentally we derive everything in lean. Heather's course looks great, although again the focus seems to be on learning how to prove the things rather than on learning the things, if you get me?

[Kevin Buzzard]

I would not recommend learning maths and learning lean at the same time -- the cognitive load is too great.

[Jireh Loreaux]

"learning how to prove things rather than on learning the things": in general I would argue that these are the same, but there can be some small amount of daylight between them. In any case, we don't have textbooks written in Lean yet.

[Johan Commelin]

Does https://link.springer.com/book/10.1007/978-3-031-14649-7 qualify?

[Matthew Pocock]

Jireh Loreaux said:

"In any case, we don't have textbooks written in Lean yet.

Thanks.

[Jireh Loreaux]

Oops, apparently I misspoke! Also, I forgot about "How to Prove It with Lean" :face_palm:

[Patrick Massot]

Johan Commelin said:

Does https://link.springer.com/book/10.1007/978-3-031-14649-7 qualify?

That book teaches a very exotic dialect of Lean 3.

[Patrick Massot]

I think Heather's book is the closest we have for Matthew.

[Matthew Pocock]

Thanks everyone. I'm going to work through Heather's book. That should keep me occupied for a bit.

[Heather Macbeth]

To Lean-ify my intro-to-proof course, I started from the kinds of arguments I wanted them to write on paper, and reverse-engineered Lean tactics to represent these arguments faithfully. Sometimes a suitable tactic was in mathlib already, sometimes I needed to write a more powerful tactic than was yet in mathlib, sometimes I needed to weaken an existing tactic so that it wouldn't do too much of the argument.

[Heather Macbeth]

I think it would not be impossible to do the same reverse-engineering process for a calculus course, which is what Matthew wants:
Matthew Pocock said:

I guess I'm looking for something more like "math 101 - equations, limits, calculus, oh my!" where incidentally we derive everything in lean.

But certainly no one has done this yet.

[Utensil Song]

Johan Commelin said:

Does https://link.springer.com/book/10.1007/978-3-031-14649-7 qualify?

The Lean proofs in the book are very close to the corresponding pen-and-paper version, and they seem easy to port to Lean 4.

It feels that the writing style is quite approachable to newcomers, so it might be a good example for when it's helpful to learn math and Lean at the same time: 1) the reader has a certain mathematical foundation; 2) the math to learn is a new specialized topic (so elements in it are not totally new to the reader); 3) there are many pen-and-paper style Lean proofs for it. 3 is the crucial part.

I thought reading Mathlib Lean proofs could help me understand the corresponding math, but it turns out to be very demanding for both my math knowledge and Lean skills, as well as the ability to bidirectionally map them when De Bruijn Factor varies significantly:

1. High for basic concepts in an area: definitions or theorem statements are short (and relatively intuitive) in math , but lots of work in Lean to work through the proper type abstraction, to adjust what's less usable or missing in the type class hierarchy etc.
2. Too low for basic proofs: there's a lot of automation for easy proofs, but when one is learning new math, they need to work out all the trivial/"obvious" details, tactics are too powerful in this stage, they will "do too much of the argument", so one can gain less insight by proving them in Lean
3. High for advanced proofs: the automation that matches the comfortable reasoning granularity or logical structure in pen-and-paper proofs are usually yet to be developed, the existing proofs might be long raw ones, or short one yet too Lean-technical.

So there are at least these 3 parts of work (to balance the De Bruijn Factor) to help one learn math and lean at the same time.

[Martin Dvořák]

Johan Commelin said:

Does https://link.springer.com/book/10.1007/978-3-031-14649-7 qualify?

Unfortunately, it seems [note that my impression might be wrong; I saw only the first two pages of every chapter] that the book uses pen-and-paper mathematical notation and then translates things into Lean. I wish [and I know that my opinion is very unpopular] they used Lean notation only, all the time (I'd suggest they should write plenty of informal (English) sentences (as they do) but, whenever a mathematical expression appears in it, it should be written in Lean).

[Matthew Pocock]

Martin Dvořák said:

whenever a mathematical expression appears in it, it should be written in Lean.

I think perhaps if the IDE had tight support between lean code and latex rendering, this would be less of an issue. Sometimes the lean code of a system of equations doesn't look much like them, but a simple typesetting/rendering would get you >90% there. Think overleaf but for interactive proofs.

[Martin Dvořák]

Matthew Pocock said:

I think perhaps if the IDE had tight support between lean code and latex rendering, this would be less of an issue.

Do you want to have a different look (of Lean expressions) in the code vs in the infoview?

[Matthew Pocock]

Martin Dvořák said:

Do you want to have a different look (of Lean expressions) in the code vs in the infoview?

Perhaps -- at least as a toggle. I can imagine that if the infoview representation is very different from the source code, it will be difficult to use the one to debug the other. But the IDE could preview the markdown in /-! -/ comments, for example, and in that view it could do a nicer rendering of the lean source code. Either in a separate preview tab, or block by block in the editor itself or infoview. There are various markdown plugins for vs code that do this kind of thing fairly well. And the Julia vs code plugin has really good dynamic content rendering including plotting charts.

[Patrick Massot]

This is coming. Kyle Miller and I already have a framework to convert Lean expressions to LaTeX but it's not hooked with the infoview yet, it's used only by our informal Lean project (see my IPAM talk from February if you don't see what I'm talking about).

[Matthew Pocock]

I hope I haven't come across as rude or entitled in this thread. Reading back over it, I do sound a bit like I'm asking for the moon on a stick. I know from personal experience the hours and coffee that goes into writing and maintaining teaching materials. And the time and swearing that goes into developing tooling. Lean is already far better than most "research" software out there.

[Matthew Pocock]

Patrick Massot said:

see my IPAM talk from February if you don't see what I'm talking about.

Just watched it on youtube - great talk.

[Kevin Buzzard]

Getting the moon on a stick is the kind of thing some of us want to aim for. There is huge potential for new kinds of mathematical literature here and there are certainly people interested in exploring the possibilities. You're definitely not coming over as rude or entitled! What's important here is different people experimenting with different ideas and then seeing what works.

[Kevin Buzzard]

As a totally different example I'd like to one day see a web page which starts with a claim that Fermat's Last Theorem is true and then lets you see more and more explanations of why depending on where you click, enabling you to go right down to the axioms if necessary whilst maintaining readability and also perhaps an overview of the structure of the proof. I've been thinking about this recently and I realise that actually I'm extremely vague on the details of how this might look in practice. There are lots of interesting questions here.

[Ruben Van de Velde]

I think I'm gonna need a bigger screen by that time :sweat_smile:

[Kevin Buzzard]

Bigger screens are already available. It's formalised proofs of Fermat's last theorem that we're missing. But I think we're also missing ideas about ways to present a super-large proof.