I think a lot of the art will be getting the computer to emit proofs in a form amenable to human understanding.
You know all those famous problems that were solved recently? How do you know they were actually solved? Maybe the Math professors are just pretending to check each others' proofs, playing a gentleman's game, and they don't want to admit that these achievements were wrong?
How do you know? Do you really want to spend 5-10 years learning enough to check one of these proofs?
If it's a computer-generated proof, and people checked the source code but can't read the proof (because it's terabytes of details), is that a valid proof? It isn't really leading to any greater understanding.
That's just flat out not true. In fact I would hazard a guess that the reverse is true (0.1% of math papers are incomprehensible to most). Not to say that math is simple but that just because something is highly specialized does not mean it is incomprehensible. Of course my only evidence is that the vast majority of specialized physics papers that I read only require some background in quantum mechanics, statistical mechanics and some of the problem domain. I read some papers in math journals too and feel like they're about on par in general.
There are certainly some mathematicians that publish in super highly specialized fields that are remarkably difficult to understand but these are a teensy tiny minority.
For example, I'm interested in optimization/signal processing/machine learning and finishing up my education. In the related journals I can barely understand the notation and miss the higher level concepts.
On the other hand I'm taking a class that required me to read a journal paper written by the professor. It was strange: I could understand it. I followed it and most of the finer details too.
I would say that OPs statement is true: 99.99% of papers published by math profs are incomprehensible to almost everyone. Not only do they use foreign notation there's also a lot the don't say because it's assumed the reader knows enough to prove it -- hence "left as an exercise for the reader..."
Granted a lot of topics may take a couple of years to understand, or even a decade. But guess what, it took the author that long to understand it too.
- there are as many odd integers as integers.
- 0.99999999... equals 1.
But it also depends on what you call 'math'. Applied math often is 'easy'. Modern abstract math, I am convinced 90+% will never be able to read, and 99% of the rest would need serious study. I know I can't make heads or tails from many papers, and I do have a M. Sc. in math. That's partly because I am rusty, but there also are lots and lots of terms in areas that I never heard about in areas such as algebra that I barely studied. For an example, look at http://mathworld.wolfram.com/search/?query=cohomology&x=0&y=..., pick any page, and check whether 'most' would be able to comprehend it.
The other replies here all seem to be "Pssh, I can already read math, and I'm a layman."
As a counterpoint, I often try to read my friends' crypto or applied math papers and literally cannot imagine understanding any of it, even given infinite time. Some stuff is just so opaque to me that I'm pretty sure it's permanently unattainable for someone with my intelligence. At the very least I'm much further than 10 years from following the state of the art in big-boy mathematics.
I would gladly use computerized comprehension-improving tools if I could get them, but then again I'm just a dumb engineer.
"A fully automatic problem solver with human-style output"
M. Ganesalingam, W. T. Gowers