## Stream: graph theory

### Topic: meta

#### Jalex Stark (Aug 12 2020 at 01:12):

Hi @Bhavik Mehta @Aaron Anderson @Alena Gusakov @Michael Hahn @Kyle Miller ! there are several somewhat independent threads of development on graph theory with the intent to PR code to mathlib.

#### Jalex Stark (Aug 12 2020 at 01:12):

Michael has a repo with code copy-pasted from Kyle and Aaron's PR, which has useful local changes that haven't propagated back to the PR.
And Alena has code copied from michael's repo with the same properties.
(Both of these are my fault, really.)

#### Jalex Stark (Aug 12 2020 at 01:15):

(this one I might have the details wrong) Bhavik recently started proving freek 83 without knowing that aaron already has a working proof in the branch mathlib:freek_83_friendship_theorem

#### Bhavik Mehta (Aug 12 2020 at 01:16):

Yup, this is true

#### Jalex Stark (Aug 12 2020 at 01:17):

Also, Michael and Alena are young and maybe not super skilled at coming up with the right places to ask questions

#### Jalex Stark (Aug 12 2020 at 01:18):

Michael's in high school, Alena just finished undergrad but doesn't have any papers under her belt, but they're both good enough at writing lean code to be useful in projects like this

#### Jalex Stark (Aug 12 2020 at 01:19):

some of you are older and want academic jobs, so you should be incentivized to want to practice some mentoring in this direction

#### Jalex Stark (Aug 12 2020 at 01:19):

so part of the point of this stream is as a focal point for organization

#### Jalex Stark (Aug 12 2020 at 01:20):

and part of the point is to provide a place to post half-formed questions or complaints or ideas (where "complaint" means "complaint about parts of the API that are still far from polished)
at the very least, I am excited to move some of these conversations out of my private messages

#### Bhavik Mehta (Aug 12 2020 at 01:25):

I should mention here as well that I've done a proof of infinite hypergraph ramsey's theorem a while ago, as well as a special case of finite ramsey's theorem too. I've also done some other basic graph theory things like the handshaking lemma, and a ton of other combinatorics in Lean, so I have a reasonably good idea about what works nicely and what doesn't. I also did something close to a lower ramsey bound to test if the probabilistic method is possible (it is)

#### Jalex Stark (Aug 12 2020 at 01:27):

I think everyone in this stream has permissions to invite other people to this stream. All of the stream history is readable by new people that join. I think the correct policy is just like the one for mathlib, "admit anyone who makes a believable claim that they want to contribute to graph theory PRs"

#### Simon Hudon (Aug 12 2020 at 02:12):

Thanks for the invite!

#### Jalex Stark (Aug 12 2020 at 02:28):

This stream is currently 8 people. I think if it ever got to 50, it should be public instead. (the true threshold is lower, 50 is just an upper bound)

#### Aaron Anderson (Aug 20 2020 at 04:21):

I've just started a branch at mathlib:graph-stream with a bunch of small definitions on top of my PRs.

#### Aaron Anderson (Aug 20 2020 at 04:22):

My hope is that we can try to combine some of our definitions there, test which definitions fit together well, and find out what basic ideas are actually missing that we need to resolve in order to start proving interesting things.

#### Kyle Miller (Aug 20 2020 at 11:45):

Nice additions. For some competition, I've ported most of the changes over to mathlib:simple-graphs2, including adjacency matrices. https://github.com/leanprover-community/mathlib/tree/simple_graphs2/src/combinatorics

This branch has simple graphs, subgraphs, spanning subgraphs, and a uniform interface to interact with them. (No induction principles yet, though.)

• I'm not sure why you defined locally_finite to be a class. Maybe so you can type less when you define the fintype.locally_finite instance? It's better as a reducible definition.
• I would have thought a graph embedding means the image is any a subgraph, but according to your definition the image is an induced subgraph. I've changed this in simple-graphs2 to match the usual notion.
• The definition of graph colorings is incorrect, I think. What you have is checking that a graph is an empty graph with up to k vertices. (It would also be nice to let the coloring set be arbitrary, since there are some interesting theorems involving countably versus uncountably many colorings.)
• It seems you based the branch on an older version of #3458?

#### Aaron Anderson (Aug 20 2020 at 16:46):

I’ll look in more detail at what you’ve done, @Kyle Miller , but I think I’d prefer if we work on the same branch, even if that means in different files, just so that we have a hope of comparing and combining things directly.

#### Aaron Anderson (Aug 20 2020 at 16:47):

Does that sound reasonable, and which do you prefer we move to?

#### Kyle Miller (Aug 21 2020 at 19:20):

I don't really understand why having everything in the same branch makes anything easier, since these are two branches in the same repository (git has many ways to compare branches with each other and with master). I'll be watching mathlib:graph-stream and incorporate ideas into mathlib:simple_graphs2, and I invite everyone to draw from the latter.

I used the word "competition" here because one of the things we're collectively trying to work out is what the definition of a simple graph should be. I believe strongly that we need to make sure derived objects like subgraphs should be graphs in their own right, in a way that generalizes to other combinatorial objects, and in the branch you created it seems you do not agree (that's probably not a fair characterization -- it would be nice to know what design constraints you feel are not being satisfied by mathlib:simple_graphs2 or how you thought this branch might be incorporated or not into mathlib:graph-stream -- I know you know branch exists and has been undergoing active development.)

For more discussion about subobjects, and for a variation on the mathlib:simple_graphs2 approach, take a look at the topic about matroids in the #maths stream. I'm thinking it's conceptually better to say a type has a way to interpret its terms as graphs, rather than saying a term of a type has a way to be interpreted as a graph, so I am considering switching the mathlib:simple_graphs2 branch to this approach. It opens up some possibilities involving extension of the simple_graphs typeclass. (I want to emphasize that I'm not attached to any particular way of doing things, and whatever satisfies the design constraints in the end is OK with me. Maybe this comes from my time as a software engineer, but in this prototyping stage I tend to think of code as something completely disposable -- my waffling on implementation serves to crystallize the constraints.)

It would be nice if there were a way to let (G : simple_graph W) be an abbreviation for "a graph-like object obtained in any way, having vertex type V". There just doesn't seem to be any way to do that except for writing something like {α : Type v} [simple_graphs α] (G : α) {H : W = V G}. (There is probably some metaprogramming that could generalize statements like this, but it's not clear at this point whether this is a principled application of metaprogramming.)

Anyway, right now we're pretty much at the second page of a GTM book on graph theory. It would be nice to progressively go through and formalize a few more pages (or chapters!) to better see how to proceed :smile:

#### Aaron Anderson (Aug 21 2020 at 20:40):

lol we maybe have all of Bollobas Page 2

#### Aaron Anderson (Aug 21 2020 at 20:41):

while you can compare between multiple branches in terms of what text they contain, you can't prove relations between definitions on different branches

#### Jalex Stark (Aug 22 2020 at 03:12):

sure, you can rename files appropriately, merge the other branch into you, and then do whatever comparison you like

#### Alena Gusakov (Aug 24 2020 at 22:21):

I pushed a little error fix that Kevin helped me out with

#### Alena Gusakov (Aug 24 2020 at 22:22):

Basically just got rid of the problem in degree_le where Lean didn't know why we were allowed to compare the degrees because it didn't know degree (G'.in_subgraph hv) is a fintype

#### Jalex Stark (Aug 24 2020 at 22:23):

what branch did you push code to? can you make a new topic instead of using this very general one?

#### Alena Gusakov (Aug 24 2020 at 22:23):

branch#simple_graphs2

Last updated: May 08 2021 at 22:13 UTC