Zeilberger, Hersh, Davis, Haken, Appel, four color theorem, computer mathematics, computerized mathematics
Part 1. Mathematics as a social phenomenon Let's start our exploration with something indisputable  let us consider mathematics as the wellknown social phenomenon. We can see that: 1) There exists a specific kind of people, most of them are wearing glasses, but don't wear ties, and they call themselves mathematicians. 2) Universities are offering study programs in mathematics, supported by chairs of mathematics. One can obtain a mathematical education. By fulfilling a specific prescribed ritual one may become Ph. D. in mathematics. 3) By fulfilling a specific prescribed ritual one can obtain goverment funding for a mathematical research. 4) People are organizing mathematical conferences and publishing mathematical journals. By fulfilling specific prescribed rituals one can achieve participation in these conferences and publish mathematical papers. Could these observations serve as a kind of "definition" of mathematics? Or, any kind of science, pseudoscience and even antiscience could be "defined" in this way? But, nevertheless... 

Mathematics  (no more than) a social ritual? In 1972, Philip J. Davis expressed serious doubts that many "mathematical facts" regarded generally as objectively established, are, in fact, probabilistic statements: Philip J. Davis. Fidelity in mathematical discourse: Is one and one really two? American Mathematical Monthly, 1972, 79(3):252–263. After this, P. J. Davis and Reuben Hersh developed this approach concluding that the generally alleged absolute objectivity, precision and rigour of mathematics is an illusion, and that the social aspect of mathematics is essential and unavoidable: "In the real world of mathematics, a mathematical paper does two things. It testifies that the author has convinced himself and his friends that certain "results" are true, and presents a part of the evidence on which this conviction is based." P. J. Davis and R. Hersh. Rhetoric and mathematics. In J. S. Nelson, A. Mcgill & D. N. McCloskey (Eds.), The rhetoric of the human sciences. Madison: University of Wisconsin, 1987, pp. 5369. Hersh and Davis advocate the view that mathematics is essentially a social phenomenon. I would prefer a less honorable term instead  social ritual (as there are many rituals in use in the human society...). Couldn't mathematicians be interested in positioning ("legalizing") mathematics as a specific social ritual? Or, they would be interested, but not ... explicitly? Could we admit publicly that mathematics is not an "objective science" (whatever it means), but an exclusive social ritual by means of which a narrow group of people is gaining both satisfaction and material benefits? [Added December 7, 2008. Thanks to Maris Ozols.] HershDavis' main argument (as of 1987) sounds as follows: "The Automath approach represents an unrealizable dream... The myth of totally rigorous, totally formalized mathematics is indeed a myth." (ibid.). Now, 20 years later, the situation is changing... See Notices of the AMS, Special Issue on Formal Proof, Vol. 55, N 11, 2008 (available online). 

Mathematics at its limits The ritual component of mathematics becomes especially noticeable in the discussions around the most complicated mathematical proofs. When solving mathematical problems of evergrowing complexity, aren't mathematicians approaching the limits of human abilities? (For computer science people, the answer would be: "Yes, obviously".) On June 23, 1993, after 7 years of hardest work, Andrew Wiles announced that he had a proof of Fermat's Last Theorem (stated some 350 years before). But preparing the proof for publication, he discovered an error. Working hard for another year, on September 19, 1994 he came finally to an idea allowing to complete the proof: A. Wiles. Modular elliptic curves and Fermat's Last Theorem. Annals of Mathematics, Volume 141 (1995), pages 443551. Thus, the essence of Wiles' proof is more than 100 pages long. Is this extremely complicated proof, now, finally, errorfree? How do mathematicians justify their confidence in this? The most distinguished experts came to a consensus that, "the proof is, finally, complete and correct"? Similar situations appear in mathematics over and again: from time to time fallacious proofs of some famous mathematical conjectures are announced (among them  some very serious proofs included): Riemann's Hypothesis, Twin Prime Conjecture etc. At best, after correcting of the actual error, the next one is discovered... Of course, this does not mean that some of the famous mathematical problems will not be solved  as was solved Fermat's Last Theorem, and recently, Poincare's Conjecture (stated in 1905, and proved in 2002 by Grigory Perelman / picture). But will this always mean that the proposed "finally correct" extremely complicated mathematical proofs are always, indeed, errorfree? Or, the conclusion will sound as usual  almost "ritually": the most distinguished experts came to a consensus that, "the proof is, finally, complete and correct"? Still, the situation is even worse around the most complicated mathematical proof ever (Classification Theorem of Finite Simple Groups)  as noted by Michael Aschbacher: "To my knowledge the main theorem of [AS] closes the last gap in the original proof, so (for the moment) the Classification Theorem can be regarded as a theorem [marked by me  K. P.]. On the other hand, I hope I have convinced you that it is important to complete the program by carefully writing out a more reliable proof in order to minimize the chance of other gaps being discovered in the future." Michael Aschbacher. The Status of the Classification of the Finite Simple Groups. Notices of the AMS, August 2004, vol. 51, N 7, pp. 736740(online copy available). "Conventional wisdom says the ideal proof should be short, simple, and elegant. However there are now examples of very long, complicated proofs, and as mathematics continues to mature, more examples are likely to appear. Such proofs raise various issues. For example it is impossible to write out a very long and complicated argument without error, so is such a ‘proof’ really a proof? What conditions make complex proofs necessary, possible, and of interest? Is the mathematics involved in dealing with information rich problems qualitatively different from more traditional mathematics?" M. Aschbacher. Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, October 15, 2005, vol. 363, N 1835, pp. 24011406 (online copy available). Should the opinion of "the most distinguished experts" admitted as the final criterion of "truth" in mathematics? 

The FourColor Theorem Exactly 30 years ago, in 1976, another bad evidence appeared: when solving mathematical problems of growing complexity, mathematicians are, indeed, approaching the limits of human abilities! FourColor Theorem. Any political map can be colored by using 4 colors in such a way that no two states sharing a common border receive the same color. As a conjecture, this statement was proposed by Francis Guthrie in 1852, but its proof was completed  in an uncommon way!  only in 1976 by Kenneth Appel and Wolfgang Haken. They spent 4 years improving and running their computer programs for about 1200 hours, checking in this way 1476 configurations necessary to establish the truth of the FourColor Conjecture. No human mathematician is able to perform this analysis manually, or even only to verify case by case the results provided by the computer! During the years after 1976, the fourcolor proof procedure was improved, the search scope was reduced to 633 configurations. But, human mathematicians still are not able to fully verify the results provided by the computer. For details, see The Four Color Theorem, 1995, by Robin Thomas. The most impressive success: in 2004 the best of the known proofs of the FourColor Theorem (together with the corresponding computer program) was completely formalized, and its correctness was checked (and approved) by using a universal tool  Coq proof assistant. For details, see A computerchecked proof of the Four Colour Theorem, 2004, by Georges Gonthier. But this does not change the situation for us, humans: human mathematicians still are not able to fully verify the proof of the FourColor Theorem. We ask a question, and the computer prints out tens of meters of paper containing the answer... 

Not our kind of persons? When preparing this lecture in June 2006, only after a long Internet search I found two pictures of Wolfgang Haken and Kenneth Appel: European Mathematical Society, Newsletter No. 46, December 2002, pp. 1519. Now, except the above
ones, how many pictures of Haken and Appel can be found
on the web? BTW, Does this mean that, for mathematicians, Haken and Appel are not their kind of persons? Could this unpleasing situation be created by the strange discussions immediately after 1976, when some (otherwise serious) people asked: "In which sense" the FourColor Theorem is "proved"? Is the result of Haken and Appel "proper mathematics"? Perhaps, for mathematicians, Haken and Appel are not their kind of persons, in the same sense as, for chess players, are not their kind of persons the programmers who created the IBM Deep Blue program that defeated Garry Kasparov in 1997? (See details of Game 6.) 

Two other famous computer assisted proofs 1989: Nonexistence of Finite Projective Planes of Order 10 For the setting and history, see Projective plane, Wikipedia, the free encyclopedia. Clement W. H. Lam, John McKay, Larry Thiel, Stanley Swiercz (see picture of the 4) and their colleagues started to work on a computer assisted solution in 1980. It took 9 years to complete (in January 1989). Lam, C. W. H.; Thiel, L.; and Swiercz, S. "The Nonexistence of Finite Projective Planes of Order 10 (15 January 1989)", Canad. J. Math. 41, 11171123, 1989. From the Abstract. "This note reports the result of a computer search which shows that no 19point configuration can be extended to a complete finite projective plane of order 10. Previous work has shown that such a plane, if it exists, must contain 24,675 19point configurations. Together, these results imply the nonexistence of a projective plane of order 10. ... It also argues that, even when the possibility of undetected software or hardware errors is taken into account, the probability is very small that an undiscovered plane of order 10 is missed by all the computer searches." pp. 67. "Table 1 lists the cases with outside intersections. These cases are easy enough to be handled by a collection of five VAX computers at Concordia [University]. ... Even with this reduction, the total computing time used at Concordia was the equivalent of 800 days of CPU time on a VAX11/780. Table 2 lists the cases with no outside intersections, which were run on a CRAY1A [supercomputer] and took an estimated 2,000 hours of computing." 1998: Kepler Conjecture about the Densest Sphere Packing in Space Stated in 1611 by Johannes Kepler (15711630): the densest possible packing of equal spheres in space is the "natural one, face to face". See figure from Kepler's pamphlet. This conjecture became part of Hilbert's 18th problem. For the setting and history, see Kepler conjecture, Wikipedia, the free encyclopedia. Thomas C. Hales and Samuel P. Ferguson started to work on a computer assisted proof in 1992. It took 6 years to complete (in 1998). Results were posted as a series of 8 preprints at http://lanl.arxiv.org/: 1. Thomas C. Hales. An Overview of the Kepler Conjecture, 16 pp. (see pp. 1112 for an account of computer involvement). ... 7. Samuel P. Ferguson. Sphere Packings V, 54. pp. 8. Thomas C. Hales. The Kepler Conjecture, 62 pp. See also Thomas C. Hales. Sphere Packings in 3 Dimensions, 3 pp. "... the proof takes over 270 pages of mathematical text, extensive computer resources, including 3 gigabytes of data, well over 40 thousand lines of code, about 10^{5} linear programs each involving perhaps 200 variables and 1000 constraints." 

Which proofs should be trusted as more reliable? Which proofs should be trusted as more reliable than the other ones  computer assisted proofs, that can't be fully verified by humans, or hypercomplicated "purely manual" human mathematical proofs? Which proofs could more likely contain errors? In fact, there is no such dilemma. None of the above mentioned computer assisted proofs is a purely "computerized proof". All of them are "using massive computer calculations on top of some mathematics" (as put by Eric W. Weisstein), i.e. the humanmathematical part of these proofs may be no less serious than complicated purely human proofs. The usual schema is as follows. Some mathematical problem is noticed to be solvable by a massive search process. The conjecture will be verified as true, if the search result will be negative, i.e. one must wait for the end of the entire process. Unfortunately, if straightforward simple search algorithms would be used, then the computation process would last for thousands of years. Now, to reduce the necessary search time to a year or less, "some mathematics" must be created, i.e. one must propose a much more clever algorithm (reducing the search space, improving the speed). After this, the actual search must be performed, using one or more computers, interrupting and restarting the process many times, correcting programming errors etc. But, of course, one must also prove that his/her clever algorithm is correct. This represents the "human part" of the computer assisted proof, and may take 100 or more pages of a published paper. Thus, essentially, from the reliability point of view, there is no difference between computer assisted proofs and complicated "purely human" mathematical proofs. But, of course, computer assisted proofs, as a rule, "achieve more"... See also: C. W. H. Lam. How reliable is a computerbased proof? The Mathematical Intelligencer, 1990, 12(1), pp. 812. 

Computer mathematics against human mathematics? Computer assistance extends the limits of human mathematical abilities. What will it be like  the future mathematics, accessible to humans only in part? Having equal mathematical abilities, mathematiciansprogrammers will, as a rule, achieve more than mathematicianspencil writers. Doron Zeilberger perceived here an analogy with the new situation around the chess game. After IBM Deep Blue program defeated Garry Kasparov in 1997, human chess players can compete seriously only among themselves. They can't hope to win the most advanced chess playing computer programs. In future mathematics, the situation may be similar: "purely human" mathematicians (rejecting the computer assistance) will be able to develop only their restricted "amateur" mathematics. Complexity of many mathematical problems exceeds human abilities... D. Zeilberger. Theorems for a Price: Tomorrow's SemiRigorous Mathematical Culture, Notices of the Amer. Math. Soc., 1993, vol. 40, no. 8, pp. 978981 (online copy). D. Zeilberger. "Real" Analysis is a Degenerate Case of Discrete Analysis. In "New Progress in Difference Equations", edited by Bernd Aulbach, Saber Elaydi, and Gerry Ladas, (Proc. ICDEA 2001), Taylor and Frances, London, 2001 (online copy). D. Zeilberger. Opinion #57, 2003, http://www.math.rutgers.edu/~zeilberg/Opinion57.html. This completes our first flow of associations. 
Zeilberger, Hersh, Davis, Haken, Appel, four color theorem, computer mathematics, computerized mathematics