Should Machines Replace Mathematicians?

I'm going to quote from Treasure Island by Robert Louis Stevenson:

> "Why, we're all seamen about here, I should think," said the lad Dick.

> "We're all foc's'le hands, you mean," snapped Silver. "We can all steer a course, but who's to set one? That's what all you gentlemen split on, first and last. If I had my way, I'd have Cap'n Smollett work us back into the trades at least; that way we'd have no blessed miscalculations and a spoonful of water a day."

That is, theorem provers may be great. Who's going to create the new theorems? Who's going to create interesting, breakthrough new theorems? The machines? Not yet, they aren't (if ever).

CAN machines replace mathematicians?

They might be able to replace an average persons need to use algebra, as they have for me, but I suspect they're not gonna replace a prize winning mathematician unless they are AGI.

Article by the same author back in 1993, "The Death of Proof"

https://www.scientificamerican.com/article/the-death-of-proo...

Some key quotes for the tldr crowd:

> Anthony Bordg, a mathematician at the University of Cambridge, worries that his field could face a “replication crisis” like that plaguing scientific research.

> Researchers at Microsoft have already invented an interactive theorem prover (https://leanprover.github.io/) called Lean that can check proofs and even propose improvements—much as word-processing programs check our prose for errors and finish sentences for us.

> Advances in computer-aided mathematics ... raise a profound question: what is the purpose of mathematics? ... worries that tools such as Lean will encourage a “stunted vision” of mathematics as an economic commodity or product rather than “a way of being human.”