Zulip Chat Archive

Stream: graph theory

Topic: hedetniemi branch


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

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

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

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 (Aug 12 2020 at 01:24):

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

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

david wärn?

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

Yeah

Aaron Anderson (Aug 12 2020 at 03:45):

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 (Aug 12 2020 at 03:46):

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

Bhavik Mehta (Aug 12 2020 at 14:40):

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 (Aug 12 2020 at 23:11):

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 (Sep 15 2020 at 16:04):

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

Aaron Anderson (Sep 15 2020 at 16:27):

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 (Sep 15 2020 at 16:30):

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 (Sep 15 2020 at 19:38):

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 (Sep 15 2020 at 19:39):

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

Bhavik Mehta (Sep 15 2020 at 19:39):

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 (Sep 15 2020 at 19:40):

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

Johan Commelin (Sep 15 2020 at 19:40):

The other stuff shouldn't be so hard.

Bhavik Mehta (Sep 15 2020 at 19:48):

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 (Sep 15 2020 at 19:49):

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 (Sep 15 2020 at 20:43):

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

Bhavik Mehta (Sep 15 2020 at 23:32):

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


Last updated: Dec 20 2023 at 11:08 UTC