Written: April 15, 1999
After the shameful rejection, by the editors of the Notices of the AMS, of my thought-provoking and unintentionally provocative Opinion 36 , I took the liberty of distributing it via E-mail and also agreed to my brilliant student Aaron Robertson's suggestion that he post it on sci.math. and sci.math.research.
The reactions were fascinating, and some of them are posted in the feedback section. I especially thank Andrej Bauer and Ron Bruck for making such a strong case.
Here I would like to clarify my previous `strong' opinion and react to the reactions, in general.
My REAL opinion is that Human-Proving and Programming computers to prove are Equally important and worthwhile. I agree with Hamming that the role of computations is insight, not numbers or symbols. BUT, since 99 percent of working mathematicians do not know how to program non-trivially, I dramatized it, so that you will get moving. But sometimes being too pushy backfires, I guess.
What made me very sad however, about many of the reactions, was the implication that proving is fun while programming is a dreadful chore. Quite the contrary! Programming is every bit as fun as proving, in fact it beats it. Non-trivial programming is at least as intellectually challenging and rewarding as proving. When I look at a complex Maple package that took months to write I get even more satisfaction than seeing one of my longer paper-and-pencil-proofs.
Now, Hear Yea, all you self-righteous defenders of insight and understanding. A good proof may give the appearance of understanding, but IN ORDER TO UNDERSTAND SOMETHING REALLY DEEPLY, YOU SHOULD PROGRAM IT.
Whenever I want to learn a new subject, I announce a graduate course in it, since the best way to learn is by teaching. But even better than teaching humans is teaching computers, i.e. program! Since computers will not let you wave your hands and wing it.
So it may well be true that all math will be fully automated one day, but this part of my prophecy was just for dramatic effect. I have no opinion on strong or weak AI, and dislike talking about politics and/or religion. I was mainly talking about the short-run, of how we should do research right now. And the current working habits of most mathematicians are very inefficient and inadequate, since they still have the pre-Computer-Algebra mentality.
For the short-range goal of getting as much mathematical INSIGHT and UNDERSTANDING in OUR lifetime, learn to program Maple, and/or Mathematica etc. I know it is very painful to learn something new, but once you take the trouble you would thank me! You would realize that you REALLY understand something ONLY after you PROGRAMED it YOURSELF.
Another human hang-up is micro-managing the details of the proof. Woe to the person who thinks that the Appel-Haken or Hales proofs do not give any insight. Of course, the details themselves do not, but who cares? It is the general approach, embodied in the COMPUTER PROGRAM that is chuck-full-of-insight. My only problem with the proofs of 4CT is that they involve too much human checking. The ultimate proof should be human-free, and all the human would have to do is enjoy the program.
Another misconception is that source-code is harder to read than human proof. Nonsense. A well-written, modular, and well-documented computer program is much easier and more fun to read than a long-winded human proof.
What was the main reason that I took the trouble of writing RENE? To learn Geometry! Now I am a whiz in Plane Geometry. Also, now I have a concrete and visceral feeling that it is all routine. Even though Triangle Geometry is no longer a la mode nowadays, it was very respectable until about eighty years ago, and it gives me such a kick that typing `Morley();' proves Morley's theorem in a few seconds. What is amusing is that Fields medalist Alain Connes just came with a new 3-page (admittedly beautiful) proof. But what Rene Descartes already knew, and is made explicit in my Maple package RENE, is that it is all routine. Could you imagine Alain Connes writing a paper entitled `A new proof of 21x31=651'?
So RENE is just a METAPHOR, to the growing routinization of mathematics. A more recent example is the so-called WZ theory. As recently as ten years ago two top combinatorialists, Ira Gessel and Dennis Stanton published a paper (in JCT(A)): `Short new proofs of Dixon and Saalschutz's Identities'. Now, thanks to WZ, these have the same epistemological stature as 1+1=2.
Another example is Mark Haiman's algorithmic lattice theory.
It is extremely unlikely that these are the only examples. So a very INTERESTING and FUN activity would be to try to trivialize and routinize (or, more tactfully, algorithmize) as much of known math as possible. When you do so, it becomes pointless to understand, say, Dixon's identity. It is true just BECAUSE. But the GLOBAL understanding that Dixon's identity like hundreds of others got embedded in an algorithmic framework is what is truly interesting.
In fact, Dixon's identity was a bad example. Dominique FOATA gave a gorgeous combinatorial proof, that changed my life and lead, together with Ira Gessel's equally elegant proof of Vandermonde's determinant evaluation, to my seminal proof, with Dave Bressoud of the not-yet-routine q-Dyson conjecture.
So, indeed HUMAN proofs are still welcome. But we better raise the standards. Foata's beautiful proof is a gem, but 99.9 percents of other proofs are worse than Shalosh B. Ekhad's proofs.
Also Connes's proof of Morley is such a beauty, that it is worth reading, even though the theorem is Maple-verifiable in 3 seconds. BUT all those long-winded solutions to Monthly problems are not!
Another boon for the humanists amongst us is as follows. Whenever a part of math becomes routine, we should look for replacement. So a good research program is the following do-loop
while we are alive do
trivialize and routinize all known math:
Discover new non-trivial parts of math:
od:
So the moral is, let's stop this silly fight, make up, and work together! The Foatas and the Conneses should indeed keep coming up with beautiful and insightful human proofs, that even when they prove routine facts, might very well generalize to the proofs of non-trivial facts. BUT, with EQUAL TIME and EFFORT, let's play the TRIVIALIZING GAME. And for that you better learn how to PROGRAM in Maple.
Let me conclude with a quote of Borwein, Borwein, Girgensohn and Parnes (Math Intell. Fall 1996, p. 15): `Why is Zeilberger so willing to give up on absolute truths? The most reasonable answer is that he is pursuing deeper truths'.
By analogy, we should give up local micro-managing `understanding' of individual facts, in favor of GLOBAL infra-structure understanding. And for that we MUST learn how to PROGRAM!