Lamport suggests hierarchical proofs as a possible remedy. They're somewhere in between computer verification and the current prevalent style.
Lamport acknowledges it would make writing proofs harder, while reading them easier. The style doesn't help to communicate the intuition behind a proof particularly well; it's more useful for verification. Mochizuki, for one, would have to work harder to write his proof (?) in that style.
I once tried proving the very first theorem in Cannas da Silva's book of symplectic geometry in this style. Screw that.
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.
If you are right then calling them "proofs" is misleading. The results aren't proven, just made convincing. So I guess they are "arguments" -- only detailed enough to convince others who already know enough about the entities being discussed.
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.
Again, the goal is not to convince, but to understand. Thus the ubiquitous "proof is left as an exercise for the reader".
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.
General Topology by Munkres is a good example because it has a great deal of prerequisites covered in the first chapters so you can compare how he explains eg set theory, functions, equivalence classes with what something like Wikipedia gives.
Lamport acknowledges it would make writing proofs harder, while reading them easier. The style doesn't help to communicate the intuition behind a proof particularly well; it's more useful for verification. Mochizuki, for one, would have to work harder to write his proof (?) in that style.