hedetniemi branch

Stream: graph theory

[Jalex Stark]

collectively, it seems like we've decided that "directly carve this branch into PRs" is not a good strategy

[Jalex Stark]

but actually I never spent a serious amount of effort studying it, and also I somehow don't know who wrote it, @Bhavik Mehta were you involved? (I guess I could go look at some file headers)

[Bhavik Mehta]

I wasn't directly involved, you can talk to David or Johan if you'd like

[Jalex Stark]

david wärn?

[Bhavik Mehta]

Yeah

[Aaron Anderson]

I mostly tried to roll my own simple_graph because I thought their stuff looked too complicated. I’m much less of this opinion now.

[Aaron Anderson]

(I still think the approach to paths is wrong, but I should revisit the basic graph types)

[Bhavik Mehta]

I think that they got stuck on a probabilistic method proof, if I remember correctly - it was why I tried the lower ramsey stuff in the first place

[Kyle Miller]

There are some problems with the definition of multigraphs in the hedetniemi branch. If I remember correctly, it the fact that it lacks proofs that the edge reversal equivalences are involutions. I think it's worth using hedetniemi as a guide of what kinds of things should be added, though.

[Bhavik Mehta]

With the recent momentum in graphs, is there interest in resuming/restarting this?

[Aaron Anderson]

Which part exactly? There are a lot of partial projects on that branch. I’m personally not that invested in the namesake result

[Aaron Anderson]

I am interested in reviving your Ramsey proof, although I’m also perversely hoping that the standard mathlib proof of finite Ramsey will be infinite Ramsey + compactness

[Bhavik Mehta]

I think the namesake result would be cool, partially for PR purposes and also because it's a recent bit of maths so it would be nice to have in mathlib

[Bhavik Mehta]

I was actually hoping for the same for finite Ramsey - my infinite Ramsey proof was cleaner than the finite version anyway

[Bhavik Mehta]

At some point over the next few days I want to get back to infinite Ramsey and hopefully simplify the proof, it's been a while since I wrote that so I imagine it could be improved

[Johan Commelin]

The problem with the Hedetniemi theorem is that I don't see how to get the random graph theory done.

[Johan Commelin]

The other stuff shouldn't be so hard.

[Bhavik Mehta]

Yeah - I think that part is manageable though, there's recently some improving counting API and I had a sketch Lean proof of a simpler random argument so I feel that since we have more people interested it should be doable

[Bhavik Mehta]

In particular the random graph arguments are closely related to things in other areas of combinatorics so I think there is some general interest in having it

[Aaron Anderson]

I could get interested in random graph theory - not sure how long it'll take me to learn the relevant API though

[Bhavik Mehta]

I think it's more about making the relevant API!