Small Ramsey numbers

Stream: Is there code for X?

[Michael Rothgang]

Inspired by an entry in the 1000+ theorem projects: what's the current status of the formalisation of small Ramsey numbers? I know @Bhavik Mehta has worked on this, even has a publication on it. What's the status for getting this into mathlib? Is there a declaration one can link to now?

[Bhavik Mehta]

It's not yet in mathlib but it's actually very close - there were a number of problems in Lean 4 making small ramsey numbers particularly annoying, but these are now all resolved, I think. I'm aiming to get all the definitions and small numbers in mathlib in the new year.