You can generate possible transformations from one proposition to another one, yes. But the space of possible transformations is infinite, how does the system know which ones to try? Moreover, even if you try some local transformation, how do you know that you have made progress?

A system like that could probably perform well on typical undergraduate proofs: epsilon-delta, proof that such and such a thing is a norm, etc., but it's gonna have a hard time with more difficult problems.