Zulip Chat Archive

Stream: graph theory

Topic: Random graphs?


view this post on Zulip Mauricio Collares (Feb 22 2021 at 22:07):

I read in another stream that a few people were working with formalizing a few random graph/probabilistic method applications and I would like to help and learn more about formalization efforts.
If anyone has useful pointers please let me know :)

view this post on Zulip Bryan Gin-ge Chen (Feb 22 2021 at 23:02):

Both probability theory and graphs are still underdeveloped in mathlib; for graph theory, I'd check out the code that we do have in mathlib (under combinatorics/simple_graph) and browse some old threads in this stream.

Not sure about the current status of probability theory, but I think #6242 and #6353 are some related open PRs.

view this post on Zulip Bhavik Mehta (Feb 22 2021 at 23:17):

Yeah I spent some time thinking about this a while ago with Alena - we've both been preoccupied with other things since then though. You can also check out #5574

view this post on Zulip Bhavik Mehta (Feb 22 2021 at 23:18):

I had most of the lower Ramsey bound proof using the probabilistic method somewhere, but I'm sure it's rotted by now; I put no effort into keeping it up-to-date

view this post on Zulip Julian Berman (Feb 22 2021 at 23:21):

oh wow, would love to see that (or any other formalized proof using the probabilistic method) if you ever find it

view this post on Zulip Bryan Gin-ge Chen (Feb 22 2021 at 23:28):

@Alena Gusakov made a helpful "project" on the mathlib repo which could be used to coordinate further efforts: https://github.com/leanprover-community/mathlib/projects/8

view this post on Zulip Alena Gusakov (Feb 22 2021 at 23:31):

Feel free to add stuff to it!

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 23:42):

Why not define walks as lists with a chain constraint? Then you get lots of defns and lemmas for free

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 23:43):

(that's a question about https://github.com/agusakov/math-688-lean/blob/main/src/walks.lean I guess, which isn't directly about random graphs)

view this post on Zulip Alena Gusakov (Feb 22 2021 at 23:44):

Ah I stole that file from the simple_graph_walks2 branch

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 23:46):

I'll move the question to the stream


Last updated: May 08 2021 at 22:13 UTC