Zulip Chat Archive

Stream: new members

Topic: Looking for "detailed enough" textbook


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 19 2020 at 23:28):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 23:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 19 2020 at 23:30):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 19 2020 at 23:31):

wikipedia is your friend :)

view this post on Zulip Daniel Fabian (May 19 2020 at 23:31):

would the proofs there have enough detail?!

view this post on Zulip Mario Carneiro (May 19 2020 at 23:32):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 23:32):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 23:32):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 23:33):

and you need the orbit stabilizer theorem

view this post on Zulip Daniel Fabian (May 19 2020 at 23:34):

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

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 19 2020 at 23:35):

does sound doable, then

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 19 2020 at 23:37):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 19 2020 at 23:38):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 19 2020 at 23:40):

Yup, sounds interesting for sure.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (May 19 2020 at 23:44):

obviously it should be possible.

view this post on Zulip Mario Carneiro (May 19 2020 at 23:44):

I think that's what formalization is

view this post on Zulip Daniel Fabian (May 19 2020 at 23:44):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (May 19 2020 at 23:47):

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

view this post on Zulip 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)

view this post on Zulip Daniel Fabian (May 19 2020 at 23:48):

and having the proof state is great

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (May 20 2020 at 06:14):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 20 2020 at 10:39):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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