Notice that 17 = R(3,3,3) is the only non-trivial known Ramsey number for 3 colors. Maybe developing the theory of finite Ramsey numbers would be more enlightening wrt to this formalization ?
I know Bhavik Mehta was working on some more general Ramsey Theory things at one point: github.com/b-mehta/combinatorics/blob/ee02d357a9508c84964c7a08657268a98e776728/src/inf_ramsey.lean It would also be interesting to formalize the other half of the proof that R(3,3,3) = 17, i.e. that there exists an edge 3-coloring on 16 nodes that does not have any monochromatic triangle.
![[TH] RNT vs SPG - VCT Ascension Pacific - Day 1](http://i.ytimg.com/vi/RUTkf8Detj8/mqdefault.jpg)
Impeccable content!!! This editing style fits this kind of video so well.
Notice that 17 = R(3,3,3) is the only non-trivial known Ramsey number for 3 colors. Maybe developing the theory of finite Ramsey numbers would be more enlightening wrt to this formalization ?
I know Bhavik Mehta was working on some more general Ramsey Theory things at one point: github.com/b-mehta/combinatorics/blob/ee02d357a9508c84964c7a08657268a98e776728/src/inf_ramsey.lean
It would also be interesting to formalize the other half of the proof that R(3,3,3) = 17, i.e. that there exists an edge 3-coloring on 16 nodes that does not have any monochromatic triangle.