Starting with formalizing basic abstract algebra

Stream: new members

[Chris M]

So far, I've been practicing theorem proving in Lean, but have not yet seriously attempted to learn how mathematics is formalized. e.g. I've only used the basic typing system, no inductive types or type classes.

I have read through the inductive types and type classes sections of the Lean tutorial, and my impression is that these are central to formalizing mathematics. I'd like to develop working knowledge on formalizing mathematics using these concepts.

Some questions:

• Is there broadly one correct (i.e. with good style) way to formalize groups, rings, abelian groups, in Lean? Are there good guidelines somewhere?
• What's the best way to get started on internalizing the best practices around formalizing groups, abelian groups, etc? I've read that we should define Group as a type class, not as a type, but other than that, I'm not sure how to do it. Would I get the knowledge required to formalize these things by going through the following tutorial? https://leanprover-community.github.io/mathematics_in_lean/
• My plan is to redo basic formalizations on groups and rings and compare it with the existing library. Is this a good idea or is there a better approach?

By the way, I haven't been able to find the actual definition of a group within the mathlib library. Where should I look within the algebra folder? https://github.com/leanprover-community/mathlib/tree/master/src/algebra

Also, this page gives me a dead link to groups: https://leanprover-community.github.io/mathlib_docs/

[Bryan Gin-ge Chen]

The google search might lead you to dead links since it's sometimes (often?) out of date. If you see any other broken links though, please report them here or on github!

[Bryan Gin-ge Chen]

Here's group btw: docs#group

[Jalex Stark]

I think that it's easier to learn Lean as a mathematician starting with proofs rather than definitions. Take the definitions in mathlib as given and see what you can prove with them

[Johan Commelin]

@Chris M I think that

My plan is to redo basic formalizations on groups and rings and compare it with the existing library. Is this a good idea or is there a better approach?

is suboptimal. There are still plenty of things out there that haven't made it to the library. Just pick something and start working on it. It will take 23 iterations to get it into a form that is ready for mathlib, but you will learn a lot along the way.

[Johan Commelin]

Why don't you formalise the binomial polynomials https://en.wikipedia.org/wiki/Binomial_coefficient#Binomial_coefficients_as_polynomials and prove basic properties about them?

[Johan Commelin]

Then you can PR this to ring_theory/polynomial/binomial

[Johan Commelin]

I think that's a lot more fun that redoing the basics of group theory, because you'll have the reward of contributing something to mathlib. And it's fairly self-contained.

[Utensil Song]

To answer your Q1,

• The Lean Mathematical Library paper is probably the best document on the design of the algebra library, particularly "4 Type Classes" and "5 Linear Algebra", they explained the design rationale and how it leverages the features available in Lean.
• I also like "3 Lean and its Mathematical Library" in the paper Formalising perfectoid spaces, the introduction is concise and exactly for the purpose of explaining the infrastructure to formalize a theory. You'll probably found some other interesting introduction on this in other formalizing papers, that's one good thing that a paper is mandatory to explain some backgrounds, you get a dedicated crash course usually more suited for the preparation to doing something than a general textbook or reference.
• "2. The Lean interactive theorem prover" and "3. The Lean mathematical library" in Diagram Chasing in Interactive Theorem Proving is my favorite just found very lately, it has really thorough explanation on developing a theory and proving things about it, it also completely weaves the Lean code with the usual math natural language expression together.

There're usually more than one way to formalize a piece of mathematics and you would not truly know the limitation of an approach until you hit a hard roadblock later when trying to prove something or state something in a natural way. So there would be quite some trial and error involved in the process. I recall an old Zulip chat said that you can only know how to do it right unless you have done it wrong many times. (And internalize such best practices or some intuition during the process)

Because a good definition can only be learned by bad proofs, it's important to sharpen the proving skill first (or at the some time) when you try to state some definitions and theorems for some mathematics. As a practice, groups etc. are good because they are well known and just abstract enough, but I would recommend something that's not in mathlib yet, such as the todo ones in https://leanprover-community.github.io/overview.html and try to do them in a similar way as the adjacent mathematical structures that's already in mathlib.

If you're particularly interested in group theory etc. , you might want to try and improve the https://github.com/ImperialCollegeLondon/group-theory-game . But in general, #mil is a really good practice which is quite evenly for different areas of (elementary) mathematics so you'll get a hang of anything you might be interested to do very quickly. And to answer your Q2, I guess not, #mil emphasize tactics for proving and not how to develop a theory (but I also don't know a general good guideline for that except reading the docs of existing formalized math).

And the last two paragraphs might have partially answered your Q3.

[Johan Commelin]

That's a really thorough and good answer!

[Johan Commelin]

I think this should maybe be promoted to some "getting started" page on the website.

[Johan Commelin]

@Chris M I can recommend picking anything from https://leanprover-community.github.io/overview.html
Lot's of people will love to give you advice along the way.

[Johan Commelin]

(Personally, I'm a lot less excited to help someone redo the basics of group theory. It's already in mathlib...)

[Patrick Massot]

I'm very confused to see that overview.html still live.

[Patrick Massot]

I thought it was removed in favor of https://leanprover-community.github.io/undergrad.html and https://leanprover-community.github.io/undergrad_todo.html

[Patrick Massot]

But indeed the source still exists in the repository.

[Johan Commelin]

Ooh, I hadn't realised that change already happened

[Sebastien Gouezel]

Isn't it the same file, but presented in a different way? I think I prefer the version where you can see both what has been done and what remains to be done at the same time (but it is buggy currently: the todo button hides many high level categories which are not completely done yet).

Also, a problem with both versions is that they are not easily searchable with Ctrl-F (unless you open the source). To find something, this would be my preferred method!

[Utensil Song]

Johan Commelin said:

Ooh, I hadn't realised that change already happened

Me too, I only followed to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Undergraduate.20math.20list/near/199766906 and I thought the separation is only planned.

[Utensil Song]

Patrick Massot said:

But indeed the source still exists in the repository.

That's probably because https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/deploy.sh doesn't delete rendered files (deleted or renamed) . And it's ok and safe as the deletion can be done manually if needed.

[Patrick Massot]

Indeed there is still a lot of work to do here, but Ryan disappeared and everybody is busy.

[Chris M]

@Johan Commelin @Utensil Song, The reason I thought it'd make sense to start reformalizing something that has already been done, is that it would give me quick feedback on whether I'm doing it right. I think I need to understand some basics before I can move on.

Having said that, if https://leanprover-community.github.io/undergrad_todo.html is actually up to date, I do see some topics that I would be interested in trying to formalize. I can't guarantee finishing it by any deadline, or guarantee finishing it, since I'm currently only doing this in my spare time, but I would be interested to try:

• parts of multivariable differential calculus
• Probability theory
• parts of integral calculus
• perhaps parts of topology

Would the following plan make sense?

1. go through "mathematics in Lean" #mil. Do the exercises
2. go through the existing docs of multivariable calculus and the other topics named above, and see which one makes most sense for me to do.
3. Pick a specific problem, come back to Zulip chat with a partial plan for how to do it, and ask for guidance wherever needed.

[Johan Commelin]

Sounds like a good plan. And like I said: you might actually get faster feedback if you pick an "exciting" topic, i.e., something that is low-hanging fruit, but not in mathlib.

[Johan Commelin]

Personally, I'm a "dive in and break things" type of learner.

[Johan Commelin]

So I didn't read much docs or code, but just started hacking. And then I had lots of questions here on zulip, and got lots of answers.

[Johan Commelin]

I would not pick probability theory as first subject... it's going to be hard to get that in a usable shape. It's better if an expert looks at that, I guess.

[Chris M]

Johan Commelin said:

I would not pick probability theory as first subject... it's going to be hard to get that in a usable shape. It's better if an expert looks at that, I guess.

I'm surprised by this. why is this harder than other topics? I don't usually think of probability theory as mathematically hard

[Patrick Massot]

Integrals are currently being refactored, so starting on probability is definitely the worst idea

[Patrick Massot]

Utensil Song said:

But indeed the source still exists in the repository.

That's probably because https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/deploy.sh doesn't delete rendered files (deleted or renamed) . And it's ok and safe as the deletion can be done manually if needed.

I removed that file by hand. We'll see if it messes up CI. The reason I removed it is it was no longer being updated. I'm wouldn't mind seeing a working version of this page again (I mean a page that is able to display both what is done and what remains to do).

[Johan Commelin]

Chris M said:

Johan Commelin said:

I would not pick probability theory as first subject... it's going to be hard to get that in a usable shape. It's better if an expert looks at that, I guess.

I'm surprised by this. why is this harder than other topics? I don't usually think of probability theory as mathematically hard

It doesn't have to be hard maths to make the formalisation hard. I think that in a typical argument in probability theory there is a lot of stuff going on that works just fine, but that you can't turn into a formal argument without completely changing the structure of the proof beyond recognition.

[Scott Morrison]

It turns out that writing "library quality" definitions is much more subtle than just writing definitions, and requires some experience that you don't automatically have even if you know maths+programming. So it's probably a good idea, while learning, to pick projects that don't involve lots of interacting definitions, and instead look for topics where the definitions are either already set up for you, or are very straightforward, and concentrate on learning to steer Lean by writing proofs, first.

[Scott Morrison]

(Just as examples as issues that you'll end up knowing about by the time you're writing "library quality definitions": bundling/unbundling, how/why/what for typeclasses, old/new structures, diamond inheritance, definitional equality, reducibility, simp normal forms... None of which you need to have your head around, or have informed opinions about, to write proofs. :-)

[Scott Morrison]

(Yet "setting up the basics of abstract algebra" requires thinking about all these things!)

[Johan Commelin]

Johan Commelin said:

Why don't you formalise the binomial polynomials https://en.wikipedia.org/wiki/Binomial_coefficient#Binomial_coefficients_as_polynomials and prove basic properties about them?

I still think that some topic like this is the easiest way to get started (@Chris M)