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.
The flow chart is a most thoroughly oversold piece of program documentation. -- Frederick Brooks, "The Mythical Man Month"