meta

Stream: graph theory

[Jalex Stark]

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]

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]

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

Yup, this is true

[Jalex Stark]

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

[Jalex Stark]

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]

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]

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

[Jalex Stark]

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]

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]

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]

Thanks for the invite!

[Jalex Stark]

I made a post in #general about this stream, somewhat codifying the invite policy i laid out above

[Jalex Stark]

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]

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

[Aaron Anderson]

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]

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.)

A few comments:

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

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]

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

[Kyle Miller]

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]

lol we maybe have all of Bollobas Page 2

[Aaron Anderson]

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]

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

[Jalex Stark]

branch#simple_graphs2
branch#graph-stream

[Alena Gusakov]

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

[Alena Gusakov]

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]

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

[Alena Gusakov]

branch#simple_graphs2