(One formulation of) Ramsey's theorem states that any colouring of edges of the complete graph with $4^n$ vertices with two colours will contain a monochromatic clique of size $n$. I am new to proof complexity and what interests me is the complexity of proving the upper bound using the sum-of-squares proof system. Do we know any upper bound or degree lower bounds for this question?
A related question is: which is the weakest proof system in which we know that Ramsey's theorem is provable? I am aware of a result due to Pudlák [P] which shows that this is possible in bounded arithmetic (i.e., $S_2$ and then shown by Jeřábek [J] to be $T_2^3$ precisely). Do we know of anything weaker?
[P]: Pudlák, Ramsey's theorem in bounded arithmetic, CSL 1990
[J]: Jeřábek, Approximate counting by hashing in bounded arithmetic, Journal of Symbolic Logic, 2009