Zulip Chat Archive

Stream: graph theory

Topic: graph theory PRs


view this post on Zulip Johan Commelin (Dec 02 2020 at 21:09):

Hey all (@Alena Gusakov @Kyle Miller @Aaron Anderson @Bhavik Mehta @Jalex Stark). I'm happy to see some graph theory PRs coming in. But I'm not really a graph theory expert, and I don't have a good vision for what the library should look like. I also don't have the time to become an expert :wink:
So, here's my proposal for these PRs: I will try my best to review them. But it would be very useful if you would also thoroughly review each others PRs. If you approve the PR (using the github review feature), then I will see those green checkmarks, and feel a lot more comfortable.
(Of course this means that you shouldn't give that green checkmark too hastily. I will interpret it as a statement that you don't have any comments or remarks left, and are happy with the way the PR looks like.)

view this post on Zulip Johan Commelin (Dec 02 2020 at 21:09):

That said, some general advice: (i) There are many other formalisation libraries out there on graph theory. Don't forget to take inspiration from those. (And I know some of you have already been doing this.)
(ii) Try to aim for some well-known (but not too hard) results in graph theory. Reaching such targets is good evidence that you are creating a useful library with a good API.

view this post on Zulip Alena Gusakov (Dec 02 2020 at 21:12):

Sorry about that! I think I just saw your name in some files when I was working on other PRs and wasn't paying attention to which ones they were, so in my mind I associated your name with the graph theory stuff

view this post on Zulip Alena Gusakov (Dec 02 2020 at 21:13):

The matching/perfect matching definitions are working toward Hall's Marriage Theorem and later Tutte's theorem

view this post on Zulip Johan Commelin (Dec 02 2020 at 21:17):

Alena Gusakov said:

Sorry about that! I think I just saw your name in some files when I was working on other PRs and wasn't paying attention to which ones they were, so in my mind I associated your name with the graph theory stuff

No worries. I don't mind getting pinged.

view this post on Zulip Jalex Stark (Dec 10 2020 at 20:03):

Johan Commelin said:

(ii) Try to aim for some well-known (but not too hard) results in graph theory. Reaching such targets is good evidence that you are creating a useful library with a good API.

I think Alena and Bhavik are pushing on Hall's marriage theorem, hoping to get it working in a non-mathlib project in time for the exp. math deadline?

view this post on Zulip Alena Gusakov (Dec 10 2020 at 20:08):

yeah Bhavik and Kyle are helping out

view this post on Zulip Alena Gusakov (Dec 10 2020 at 20:36):

once i'm done with my brute-force proof i'll clean it up and start slicing off into PRs


Last updated: May 08 2021 at 23:10 UTC