# Complexity of (Graph) Ramsey Theorem in Sum-of-Squares Proof System

(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

• As for bounded arithmetic, I believe nothing better than $T^1_2+\mathit{rWPHP}(PV_2)$ (which is included in $T^3_2$) is known. As for propositional proof systems, lower bounds are known for resolution (see Lauria, Pudlák, Rödl, Thapen: The complexity of proving that a graph is Ramsey) and cutting planes (Lauria: A rank lower bound for cutting planes proofs of Ramsey's theorem); I don’t know if there are any SoS lower bounds. Jul 8 at 14:34
• Thanks, Emil. I would accept that as an answer. Jul 8 at 15:22
• I suppose by $rWPHP$ you are referring to relational $WPHP$? Jul 8 at 15:27
• No, retraction-pair WPHP, as in my paper that you linked to. Jul 8 at 15:42