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.
It's a naive, domestic operating system without any breeding, but I think you'll be amused by its presumption.