Ramsey Theory/Graphs

Stream: Is there code for X?

[Mattias Ehatamm]

Hello, I'm an undergraduate at the University of Waterloo just getting started with Lean, and have been looking for a good graph theory-related project with my supervisor. I noticed some buzz about it in this chat, but is there any existing proof of the original Ramsey's Theorem in mathlib? If not, are there any significant parts of graph theory that have not been formalized yet that would be good to work on?

[Sky Wilshaw]

https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean has Ramsey's theorem but it's not in mathlib I think.

[Junyan Xu]

This seems to be the finite version; not sure why two_ramsey is commented out ...

[Bhavik Mehta]

two_ramsey is there, two_ramsey' is commented out, my vague memory of this was that I did the 2 case first, then realised the r-case should be induction where the base case is one_ramsey (which is just pigeonhole); so I tried to rewrite my proof of two_ramsey under the new name two_ramsey' to give the general case directly, but never got round to finishing it

[Bhavik Mehta]

If you haven't already seen, the channel #graph theory might be useful to you