Joe N said: >... finding proofs and generating proofs are the same >problem. They are not.
Perhaps I will be clearer to you all if I say "generating derivations" instead of "generating proofs". Typically the derivations will be generated roughly in ascending order of derivation length, by simply putting the deductive machinery of the formal system into systematic action.
So why is this so much easier than finding a proof given a proposition that wants a proof (derivation)? Given a proposition, the sought for derivation may be very long, or it may not exist at all.
This is why the two seemingly closely related activities turn out to be so very different computationally.