We devise a new combinatorial characterization for proving space lower bounds in algebraic systems like Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr). Our method can be thought as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials instead that clauses as in the case of Resolution. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution.A very simple case of our method allows us to obtain all the currently known space lower bounds for Pc and Pcr (CTn, PHPnm, BIT-PHPnm, XOR-PHPnm). The way our method applies to all these examples explains how and why all the known examples of space lower bounds for Pc Pcr are an application of the method originally given by Alekhnovich et al. (2002) that holds for set of contradictory polynomials having high degree. Our approach unifies in a clear way under a common combinatorial framework and language the proofs of the space lower bounds known so far for Pc/Pcr.

More importantly, using our approach in its full potentiality, we answer to the open problem (Alekhnovich et al. 2002, Filmus et ale 2012) of proving space lower bounds in Polynomial Calculus and Polynomials Calculus with Resolution for the polynomial encoding of randomly chosen k-CNF formulas. Our result holds for k4. Then, as proved for Resolution (Ben-Sasson and Galesi 2003), also in Pc and in Pcr refuting a random k-CNF over n variables requires high space measure of the order of (n). Our method also applies to the Graph-PHPnm, which is a PHPnm defined over a constant (left) degree bipartite expander graph. We develop a common language for the two examples.