Looking for "detailed enough" textbook

Stream: new members

[Daniel Fabian]

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]

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

[Mario Carneiro]

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

[Daniel Fabian]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

If you look at algebra.group, it's all pretty easy to follow

[Daniel Fabian]

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]

wikipedia is your friend :)

[Daniel Fabian]

would the proofs there have enough detail?!

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

and you need the orbit stabilizer theorem

[Daniel Fabian]

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

[Mario Carneiro]

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]

does sound doable, then

[Mario Carneiro]

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]

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]

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

[Daniel Fabian]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

Yup, sounds interesting for sure.

[Mario Carneiro]

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]

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

[Daniel Fabian]

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]

obviously it should be possible.

[Mario Carneiro]

I think that's what formalization is

[Daniel Fabian]

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

[Daniel Fabian]

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

[Daniel Fabian]

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]

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

[Daniel Fabian]

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

[Daniel Fabian]

and having the proof state is great

[Patrick Stevens]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

@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]

@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]

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]

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]

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]

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.