You just look for all proofs of a certain length. This is equivalent to checking if a Turing machine halts within a bounded number of steps. This is a NP problem.