[Laakeri]

For binary-encoded input it is in 2-EXPTIME by trying all graphs of size exponential in the input number and testing all subsets of the given size. Would be surprising if any hardness result for complexity classes would be known.

[ouid]

Wait, that doesn't make sense, does it? The Ramsey function grows so fast that Peano arithmetic cannot prove that it is total.

[CaptainNegative]

I'm not sure what you're referring to here. Ramsey's theorem is constructive enough that you can extract an upper bound of 4^k on the kth diagonal Ramsey number, and the (j,k)th Ramsey number is bounded from above by the max(j,k)th diagonal number.

[ouid]

My mistake. I, and I suspect the original commenter, was thinking about the strengthened finite Ramsey theorem. From wikipedia: https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...

For any positive integers n, k, m, such that m ≥ n, one can find N with the following property: if we color each of the n-element subsets of S = {1, 2, 3,..., N} with one of k colors, then we can find a subset Y of S with at least m elements, such that all n-element subsets of Y have the same color, and the number of elements of Y is at least the smallest element of Y.

This function is outside the reach of Peano arithmetic.