I studied mathematics and don't agree with this at all, for several reasons. For one the entire point of maths is that it describes a formal system in which one can 'shut up and calculate'. Mechanizing maths goes back to Leibniz and Hilbert. Nobody should surprised that the big formalism with explicit rules you invented is the first thing to yield to automation, that's why it exists.
Secondly research, including maths for a long time has been a collaboration of people, institutions, machines and processes, even maths does not consist of Faustian heroes in caves having revelations.
And thirdly just because a machine produces a 500 page proof doesn't mean your job is done. Science produces knowledge. Knowledge is information made legible to understanding by people. So there will be endless work for humans to go over machine proofs and turn it into something we understand. Just like chess computers ultimately expanded human chess.