Written: Sept. 13, 2005.
For at least twenty-five years, I have admired the deep and insightful preaching of the Omega man, Greg Chaitin. His great vision had (and has) immense influence on experimental mathematicians like myself. He also influenced profoundly other kinds of experimentalists like the Borwein brothers and their gang.
Greg's argument, that he so eloquently talked about in our last week's Experimental Mathematics Seminar, in a nutshell, is that Gödel's Incompleteness is not just a marginal curiosity for logicians and philosophers, irrelevant to practicing mathematicians, but is everywhere dense in mathematics. Hence all non-trivial statements are Chaitin-Kolmogorov incompressible, and should be taken as "axioms", or Laws of Nature, like The Second Law of Thermodynamics, say. A great metaphor are the digits of Omega.
This got me thinking that, while Chaitin's point is obviously correct, Thou shall not utter the Name of the Holy, transcendental, Omega (and Turing-Halting and Gödel-Incompleteness) in vain! The same point can be already made, much more prosaicly, by invoking intractability. All non-trivial math problems are NP hard, and all the human heuristics for arriving at so-called rigorous proofs are exponential-time algorithms, with some hidden parameter, n, say, that these poor humans do for n=1, n=2, and sometimes n=3, and they call it mainstream higher mathematics. Of course, human mathematics (for the most part) follows the path of least resistance, and picks problems that they can do. Problems that they can't do they deride, like that prototypical human, Nicolas B. (speaking through Dieudonné) as ``stillborn'' (like the odd-perfect-number problem) or at best "without issue" (like "combinatorics" (quotes in the original)). Cher Nicolas et Cher Jean, I guess that problems with issue are problems that by definition you can do.
Well, let me adapt your anthropomorphic, human-centric definition, and define a trivial problem as a problem that you (or any human, including Sir Andrew) can do, and as non-trivial any problem that you can't do. Problems that man-made computers can do, but humans (presumably and hopefully) can't, like 4CT, I call semi-trivial.
Another modification of Chaitin's vision is not to dump proofs completely. Proofs and conjectures (i.e. statements) are all mathematical objects, hence both can be found empirically, by searching. Humans still have a role, for now, by teaching the computer to do clever searching, by trimming the haystack. The "clever" version is still exponential-time (if it weren't it would have meant that the problem was trivial, which makes it uninteresting), but the exponent is smaller. So all what human mathematics does is apply implicit exponential-time algorithms, called "heuristics" to find some trivial pebbles on the shore of the (even decidable part!) of the mathematical ocean.
So we can use the computers to discover conjectures, of course, but also to discover proofs. All we need is teach our computers an ansatz and let them start searching. As trivial as current mathematics is, it would still be unwise to disregard it, and start everything from scratch. I hope that Gauss, Wiles and company won't mind if we deconstructed their proofs (whose motivations they were so careful to hide), find the underlying, implicit, ansatz, and then teach it to computers. Don't get too excited! Even computers will only be able to go a few orders of magnitude more than humans, and could only prove semi-trivial results, rigorously, and as I said elsewhere, for all non-trivial results, we would have to be content with semi-rigorous proofs, and often not even, and we should settle for non-rigorous proofs, in the style of theoretical physics, and most often, not even that. But there would be a whole spectrum.
So, let's not dump proofs completely. Proofs are just another mathematical object, and it is fun to look for them, along with other objects. But we have to be flexible, and allow all kinds of proofs.