Stream: graph theory
Topic: Random graphs?
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 :)
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.
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
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
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
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
Alena Gusakov (Feb 22 2021 at 23:31):
Feel free to add stuff to it!
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
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)
Alena Gusakov (Feb 22 2021 at 23:44):
Ah I stole that file from the simple_graph_walks2 branch
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