Random graphs?

Stream: graph theory

[Mauricio Collares]

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

[Bryan Gin-ge Chen]

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.

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Julian Berman]

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

[Bryan Gin-ge Chen]

@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

[Alena Gusakov]

Feel free to add stuff to it!

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Alena Gusakov]

Ah I stole that file from the simple_graph_walks2 branch

[Yakov Pechersky]

I'll move the question to the stream