# Zulip Chat Archive

## Stream: new members

### Topic: Looking for "detailed enough" textbook

#### Daniel Fabian (May 19 2020 at 23:27):

As an exercise that's substantial, I'd like to formalize a chunk of math from the ground up. Take it as an extended tutorial, if you will ;-).

Can you suggest a textbook about Algebra that would have enough detail that one can formalize it?

Not quite sure how ambitious it is, if you go from the axioms, but it'd be cool if I could prove, say, the Sylow theorems.

#### Mario Carneiro (May 19 2020 at 23:28):

The first Sylow theorem is proven, so perhaps you could try to do the other two?

#### Mario Carneiro (May 19 2020 at 23:28):

or does "from the ground up" mean no mathlib?

#### Daniel Fabian (May 19 2020 at 23:29):

At least in the beginning it would mean no mathlib. The goal is to get familiar with writing proofs in lean.

#### Mario Carneiro (May 19 2020 at 23:29):

You don't necessarily have to compromise on "from the ground up" even if you use mathlib; just study the mathlib source material that you want to use very carefully

#### Mario Carneiro (May 19 2020 at 23:30):

which as a side benefit will teach you a whole lot about new tactics and how to write proofs in mathlib style

#### Mario Carneiro (May 19 2020 at 23:30):

If you look at `algebra.group`

, it's all pretty easy to follow

#### Daniel Fabian (May 19 2020 at 23:31):

Then there's also the fact, that I got my degree 10 years ago and don't know any of the proofs anymore, lol :P.

#### Mario Carneiro (May 19 2020 at 23:31):

wikipedia is your friend :)

#### Daniel Fabian (May 19 2020 at 23:31):

would the proofs there have enough detail?!

#### Mario Carneiro (May 19 2020 at 23:32):

For sylow, there was enough for me to vaguely follow along enough to formalize

#### Mario Carneiro (May 19 2020 at 23:32):

https://en.wikipedia.org/wiki/Sylow_theorems#Proof_of_the_Sylow_theorems

#### Mario Carneiro (May 19 2020 at 23:32):

there is some stuff about p-groups that I hadn't heard of but nothing crazy

#### Mario Carneiro (May 19 2020 at 23:33):

and you need the orbit stabilizer theorem

#### Daniel Fabian (May 19 2020 at 23:34):

Ya, I'll need to read up on the basics again. (Hence the textbook, too)

#### Mario Carneiro (May 19 2020 at 23:34):

other than that it's just a clever choice of set for the group to act on so that the orbit stabilizer theorem applies

#### Daniel Fabian (May 19 2020 at 23:35):

does sound doable, then

#### Mario Carneiro (May 19 2020 at 23:35):

I've managed to get surprisingly far doing formalization without ever really using a textbook cover to cover, but most of the stuff I do is "general knowledge" mathematics

#### Mario Carneiro (May 19 2020 at 23:36):

for individual theorems with complicated proofs it can sometimes be helpful to shop around for a textbook with a good proof of it, but the overall architecture of how to string theorems together into a library of results is up to you

#### Daniel Fabian (May 19 2020 at 23:37):

Ya, see, when I was doing the math olympiad one, I actually enjoyed lean.

#### Daniel Fabian (May 19 2020 at 23:37):

Having the context around is quite useful when you don't have a clue what you're proving. And just looking around.

#### Mario Carneiro (May 19 2020 at 23:37):

right, if you are just thinking "let's do group theory" a textbook is a good way to turn that into some concrete goals

#### Daniel Fabian (May 19 2020 at 23:38):

Well, that was kind of the idea, to be honest.

#### Mario Carneiro (May 19 2020 at 23:38):

but another way to get concrete goals is "let's do sylow's theorems" -> "let's do orbit stabilizer theorem" -> "what's a group action" -> "what's a group" and build from there

#### Daniel Fabian (May 19 2020 at 23:39):

Yep, I could do that as well. Try to state the theorem and notice what definitions you are missing.

#### Mario Carneiro (May 19 2020 at 23:40):

the advantage of the latter method is that you are always building something with the applications in mind, so you are less likely to write it in a way where it doesn't actually easily apply to the application domain

#### Daniel Fabian (May 19 2020 at 23:40):

Yup, sounds interesting for sure.

#### Mario Carneiro (May 19 2020 at 23:41):

when you are thinking "let's do group theory" this is a real concern, and when you are working from a textbook you might end up writing in a style that is too similar to the textbook, which fits the author's applications more than yours

#### Mario Carneiro (May 19 2020 at 23:43):

it's like tactic mode, you work backward from the goal rather than forward into the unknown

#### Daniel Fabian (May 19 2020 at 23:43):

It might be an interesting challenge to take a valid proof of the theorems and then refactor them to be based on mathlib.

#### Daniel Fabian (May 19 2020 at 23:44):

obviously it should be possible.

#### Mario Carneiro (May 19 2020 at 23:44):

I think that's what formalization is

#### Daniel Fabian (May 19 2020 at 23:44):

Right now I'm not quite sure yet, where I see lean in my workflow.

#### Daniel Fabian (May 19 2020 at 23:45):

Most of what I do are algorithms but occasionally I like to prove some properties about the underlying objects are true.

#### Daniel Fabian (May 19 2020 at 23:46):

For instance not too long ago, I noticed that some criterion I used for optimization turned out to be an iff statement.

So I used that property to completely change the underlying data structure.

#### Daniel Fabian (May 19 2020 at 23:47):

And pretty much all I do is discrete math, anyway.

#### Daniel Fabian (May 19 2020 at 23:48):

I'm thinking lean might be useful for modelling the objects and proving properties (not really program verification)

#### Daniel Fabian (May 19 2020 at 23:48):

and having the proof state is great

#### Patrick Stevens (May 20 2020 at 05:00):

Mario Carneiro said:

The first Sylow theorem is proven, so perhaps you could try to do the other two?

Per entry 72 at https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md, we do actually have the other two

#### Yury G. Kudryashov (May 20 2020 at 05:06):

More precisely, there is a repo by @Chris Hughes with these proofs. They were never PR'd to `mathlib`

.

#### Chris Hughes (May 20 2020 at 06:14):

I'll probably get round to PRing them after my exams finis.

#### Kevin Buzzard (May 20 2020 at 07:34):

@Daniel Fabian if what you do now is mostly discrete maths then why don't you do some graph theory? Weren't there people working on this?

#### Daniel Fabian (May 20 2020 at 10:30):

@Kevin Buzzard That's a fine question. The answer is that I just didn't think too deeply about the choices. When I finished or was close to finishing the tutorial, Algebra happened to the first thing that came to mind.

I tend to associate Algebra mostly with things like the operations that may be allowed in a puzzle like a Rubik's cube or cryptography. Both of which would count as discrete.

That said, you are absolutely right about graph theory. That's actually something I use really a lot, so I think I will go with that, thanks.

My very next project though will be formalising some basic statements about n-way cartesian products. Specifically, how cartesian products commute with union, intersection and complement.

I recently was implementing a set datastructure that uses cartesian products as building blocks. So I know the domain and what properties I want proven.

Yet, I need to find a way how to formulate an n-way product - probably just built up inductively from pairs is fine, not sure.

#### Patrick Massot (May 20 2020 at 10:39):

What do you call an n-way product? Do you mean $X^n$ or the general case $\prod_{i=1}^n X_i$?

#### Daniel Fabian (May 20 2020 at 10:49):

The idea is, that I'm representing a set consisting of n dimensions. If a particular subset happens to be a cartesian product, i.e. there exist subsets of each dimension such that their product is the same set, then we only store that information as a "product of" along with the projections.

So I need the general prod construct.

#### Patrick Massot (May 20 2020 at 10:57):

Ok, so you want

```
def product {ι : Type*} {X : ι → Type*} (s : Π i, set (X i)) : set $ Π i, X i :=
{ x | ∀ i, x i ∈ s i}
```

I don't if we have supporting lemmas for this definition.

#### Daniel Fabian (May 20 2020 at 11:02):

Thanks! And please don't worry about the lemmas, I want to prove the properties myself anyway. I've done it on paper a while ago so it should be pretty straight-forward. I only need length and set union on each of the components, those are easy to write.

Last updated: May 12 2021 at 03:23 UTC