We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula $F$, it is NP-hard to find a refutation of $F$ in the Nullstellensatz or Polynomial Calculus proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Muller (JACM 2020) that established an analogous result for Resolution.

We retract the non-automatability result for Sherali-Adams (see footnote on page 1).

We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula $F$, it is NP-hard to find a refutation of $F$ in the Nullstellensatz, Polynomial Calculus, or Sherali--Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Muller (JACM 2020) that established an analogous result for Resolution.

Added an alternative proof via size-width tradeoffs.

We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula $F$, it is NP-hard to find a refutation of $F$ in the Nullstellensatz, Polynomial Calculus, or Sherali--Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Muller (FOCS 2019) that established an analogous result for Resolution.