Semialgebraic proofs

Propositional proof complexity is a rapidly progressing area of research. The existence of polynomial-size proofs for every propositional tautology would imply NP=coNP. So far, only lower (and upper) bounds on the complexity of proofs in specific proof systems (and for specific tautologies, respectively) are known.
The first part of the talk will contain an introduction to propositional proof complexity and a survey of known proof systems and results.
The second part of the talk concerns the results of the speaker (joint with Dima Grigoriev and Dimitrii V. Pasechnik). We study semialgebraic proofs, i.e., proofs that use reasoning about polynomial inequalities. For example, here is a proof of the propositional pigeon-hole principle:
$$ \sum_{k=1}^m\biggl(\sum_{l=1}^{m-1} x_{kl}-1\biggr)+\sum_{l=1}^{m-1}\biggl(\sum_{k=1}^m\biggl(\sum_{k\ne k'=1}^m(1-x_{kl}-x_{k'l})x_{kl}+(x_{kl}^2-x_{kl})(m-2)\biggr)+\biggl(\sum_{k=1}^m x_{kl}-1\biggr)^2\biggr)=-1. $$
(It will be explained in the talk why this is a proof.) The proofs of this tautology in many other systems have exponential (in the number $m$ of pigeons) length.