Grochow and Pitassi (2018) introduced the algebraic proof system, the Ideal Proof System (IPS), which connects algebraic circuit complexity to propositional proof complexity. They showed that propositional proof systems such as Extended Frege (Frege) are equivalent to circuit IPS (formula IPS) if the correctness of PIT for circuits (formulas) can ... more >>>