A proof system "P" is "automatable" if there is an algorithm which given a tautology formula_1 outputs a "P"-proof of formula_1 in time polynomial in the size of formula_1 and the length of the shortest "P"-proof of formula_1. Note that if a proof system is not polynomially bounded, it can still be automatable. A proof system "P" is "weakly automatable" if there is a proof system "R" and an algorithm which given a tautology formula_1 outputs an "R"-proof of formula_1 in time polynomial in the size of formula_1 and the length of the shortest "P"-proof of formula_1.