Automated proofs by contrast really are proofs but as many of these comments show are not arguments.
So maybe the problem to be solved is to appropriately connect mathematical arguments (what mathematicians call proofs) to proofs, while recognizing that they are actually two entirely separate families -- as different as plants and animals.
To extent that mathematics is a science, the whole point is to understand. Of course, people time and again have succumbed to the feeling that (e.g.) numbers are divine, but there's nothing mathematical about that.
---
It's not like it has been established as a mathematical theorem based on simpler ontological facts that capital-T truth exists. And everything in our daily experience points out to the contrary.
That fact that computers and programming languages have evolved from XOR and NAND semiconductors says a lot about the power of a particular branch of mathematics; it says nothing about the nature of mathematics. That idea is like claiming that the existence of probability theory implies that mathematics is about reasoning with uncertainties.
The proof that I eventually used in my dissertation is even wordier and with less display-mode equations than the one in the book (I became very influenced by the prose in old topology books).
Most of the time, the point of proofs isn't to establish something is true, but to communicate something about the internal structure of a piece of mathematics.
The problem with Mochizuki is that he did his work isolated from the rest of the world, so the internal structure of the kind of maths he invented is opaque. Accordingly, what mathematicians are really trying to do is to examine what makes this new maths tick; the books that make this accessible to mathematicians worldwide will not be fully-verifiable proofs of a statement, but webs of separate propositions whose statements are illuminating and whose proofs are easy to understand. If they're really successful, some may even be left as an exercise to the reader.