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.
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.