Automated proofs aren't remotely comparable to Mochizuki's abc stuff. Automated proofs just handle a lot of complicated case by case checking that humans could in principle do, it's just too much work, like counting to a trillion. Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.
Mochizuki's stuff is simply a hypercomplicated pile of nonsense unintelligible to the mathematical community.
> 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.
Mochizuki's stuff is simply a hypercomplicated pile of nonsense unintelligible to the mathematical community.