It's easy to give an algorithm that generates a proof of a mathematical theorem that's provable: choose a formal language with definitions and axioms, and for successive values of n, enumerate all sequences of mathematical deductions of length n, halting if the final line of a sequence is the statement of the the desired theorem.

~~Nitpick: This only works if the chosen formal system only contains rules that produce longer theorems.~~

Edit: Oops, looks like I misread the quote. This method will enumerate all theorems, but not (as I first interpreted it) decide if a given string is a theorem in finite time.