Sherali–Adams relaxations and sum-of-squares (SOS) hierarchies offer a unifying framework for understanding the power and limitations of algorithmic techniques in optimization and theoretical computer science, particularly in approximation algorithms and complexity theory, where lower bounds on these hierarchies translate into inherent computational hardness. In this talk we survey results concerning proof systems modeling those relaxations with a focus on understanding the strength of the systems. No previous knowledge of proof complexity will be needed. This talk is partially based on a joint work with Maria Luisa Bonet.