It’s harder. It’s also not generally possible. By Gödel’s incompleteness theorem, there are theorems that can neither be proven nor disproven. In addition, any computable axiom schema will still result in some such theorems. If you had an algorithm to prove or disprove any provable or disprovable theorem, and tell if it can’t be done, you could make a computable axiom schema to make the system complete.
It’s harder. It’s also not generally possible. By Gödel’s incompleteness theorem, there are theorems that can neither be proven nor disproven. In addition, any computable axiom schema will still result in some such theorems. If you had an algorithm to prove or disprove any provable or disprovable theorem, and tell if it can’t be done, you could make a computable axiom schema to make the system complete.
But proof finding of proofs of a specific lengths is in NP. That is “Is there a proof of X with length less than K” is in NP.