[tianlins]

I think automated theorem proving replaces the "search function" of a mathematician. But there is another part, which seems to be more important, is the creative insights. For example, inferring and conjecturing a theorem from few "data points". Machines at the moment do not have such capability yet.

[zenogais]

I think creativity is more than just inference from limited data (which computers can do also). It has to do with either discovering a way to connect two or more seemingly unconnected things or discovering a new means by which to connect two or more things.

Mechanically churning through a pre-defined possibility space doesn't seem like a sure-fire way to produce either of these effects. Though it is, no doubt, a great way to generate proofs that were previously prohibitively expensive to produce.