The job of a mathematician is to study mathematics, not to create proofs.
An automatic proof solver doesn't make mathematicians obsolete any more than the excel sheet made accountants obsolete.
An automatic proof solver doesn't make mathematicians obsolete any more than the excel sheet made accountants obsolete.
Mathematicians will soon be left only to conjecture, with proofs being automated. The issue I see is that AI will devise proofs that are beyond our comprehension, since humans are already taxing each other (cf. Wiles, Mochizuki, Perelman, etc.) Once humans lose grasp of the proof, how will they propose new conjectures?