> Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.
I would add current automated proof systems. IMHO we are just at the beginning that mathematicians realize the usefulness of technology, which was basically neglected ever since.
It will be very interesting to see what happens! A common theme in mathematics is that the proofs are the (relatively) easy part, while knowing what to prove is hard. Still, I'm sure mathematicians will welcome greater automation of the "easy" part. If machines ever do more than drudge work, there will also be the challenge of making the machine-generated proofs intelligible to humans, similar to the interpretability issues around machine learning models today.
I would add current automated proof systems. IMHO we are just at the beginning that mathematicians realize the usefulness of technology, which was basically neglected ever since.