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.