(I'm reminded of Godel's letter discussing P=NP - should such an algorithm be found, mathematicians could be replaced by a machine that searches all proofs with less than a few million symbols; anything that couldn't be proved with that many symbols would be of little to no interest to us.)

Or, at least, they could be replaced by people who can understand and seek out proofs that are relevant to us out of the arbitrarily large number of useless ones. So mathematicians basically.