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.

Doron Zeilberger's Opinion's Table of Content