If it's possible to enumerate all valid proofs I propose the following proving algorithm: Run through all valid proofs; once you get to a proof whose conclusion is the theorem you want to prove, return that proof.
[if you don't know whether your theorem is true or not, run the above algorithm on its negation as well].
What's wrong with my algorithm?
The problem is that some propositions P have the following two properties:
1: P has no proof
2: (not P) has no proof.
So your algorithm searches forever and you don't know if it just hasn't found anything yet, or if there is nothing to be found.
What is research but a blind date with knowledge? -- Will Harvey