Today

There are writings on the wall that, now that the silicon savior has arrived, a new testament is going to be written. Although there will always be a small group of ``rigorous'' old-style mathematicians(e.g. [JQ]) who will insist that the true religion is theirs, and that the computer is a false Messiah, they may be viewed by future mainstream mathematicians as a fringe sect of harmless eccentrics, like mathematical physicists are viewed by regular physicists today.

The computer has already started doing to mathematics what the telescope and microscope did to astronomy and biology. In the future, not all mathematicians will care about absolute certainty, since there will be so many exciting new facts to discover: mathematical pulsars and quasars that will make the Mandelbrot set seem like a mere Jovian moon. We will have (both human and machine For example, my computer Shalosh B. Ekhad, and its friend Sol Tre, already have a non-trivial publication list, e.g. [E], [ET] ) professional theoretical mathematicians, who will develop conceptual paradigms to make sense out of the empirical data, and who will reap Fields medals along with (human and machine) experimental mathematicians. Will there still be a place for mathematical mathematicians? This will happen after a transitory age of semi-rigorous mathematics, in which identities (and perhaps other kinds of theorems) will carry price-tags.

A Taste Of Things To Come

To get a glimpse of how mathematics will be practiced in the not too far future, I will describe the case of algorithmic proof theory for hypergeometric identities[WZ*][Z*][Ca]. In this theory, it is possible to rigorously prove, or refute, any conjectured identity belonging to a wide class of identities, that includes most of the identities between the classical special functions of mathematical physics. Any such identity is proved by exhibiting a proof certificate, that reduces the proof of the given identity to that of a finite identity among rational functions, and hence, by clearing denominators, to that between specific polynomials.

This algorithm can be performed successfully on all ``natural identities'' we are now aware of. It is easy, however, to concoct artificial examples for which the running time, and memory, are prohibitive. Undoubtedly, in the future ``natural'' identities will be encountered whose complete proof will turn out to be not worth the money. We will see later, how, in such cases, one can get ``almost certainty'' with a tiny fraction of the price, along with the assurance that if we robbed a bank, we would be able to know for sure.

This is vaguely reminiscent of transparent proofs introduced recently in theoretical computer science[Ci][ALMSS][AS]. The result that there exist short theorems having arbitrarily long proofs, a consequence of Gödel's incompleteness theorem, also comes to mind [S]. Namely, the ratio (proof length)/(theorem length) grows fast enough to be non-recursive. Adding an axiom can shorten proofs by recursive amounts [G], [D]. I speculate that similar developments will occur elsewhere in mathematics, and will ``trivialize'' large parts of mathematics, by reducing mathematical truths to routine, albeit possibly very long, and exorbitantly expensive to check, ``proof certificates''. These proof certificates would also enable us, by plugging in random values, to assert ``probable truth'' very cheaply.

Identities

Many mathematical theorems are identities: statements of type ``='', which take the form A=B. Here is a sampler, in roughly an increasing order of sophistication.

1. 2+2=4.

2. .

3. .

4. .

5. .

6. .

7. Let , then

7'. Let be as in 7.

8. Let be given by,

then

8'.

9. Analytic Index=Topological Index.

10. for every non-real s such that .

All the above identities are trivial, except possibly the last two, which I think quite likely will be considered trivial in two hundred years. I will now explain.

Why are the first 8 identities trivial?

The first identity, while trivial nowadays, was very deep when it was first discovered, independently, by several anonymous cave-dwellers. It is a general, abstract theorem, that contains, as special cases, many apparently unrelated theorems: Two bears and Two bears make Four bears, Two apples and Two apples make Four apples, etc. It was also realized that in order to prove it rigorously, it suffices to prove it for any one special case, say, marks on the cave's wall.

The second identity: , is of one level of generality higher. Taken literally (in the semantic sense of the word literally), it is a fact about numbers. For any specialization of a and b we get yet another correct numerical fact, and as such it requires a ``proof'', invoking the commutative, distributive and associative ``laws''. However, it is completely routine when viewed literally, in the syntactic sense, i.e. in which a and b are no longer symbols denoting numbers, but rather represent themselves, qua (commuting) literals. This shift in emphasis roughly corresponds to the transition from Fortran to Maple, i.e. from numeric computation to symbolic computation. Identities 3 and 4 can be easily embedded in classes of routinely verifiable identities in several ways. One way is by defining and by and , and the Fibonacci numbers by Binet's formula.

Identities 5-8 were, until recently, considered genuine non-trivial identities, requiring a human demonstration. One particularly nice human proof of 6, was given by Cartier and Foata[CF]. A one-line computer-generated proof of identity 6 is given in [E]. Identities 7 and 8 are examples of so-called q-binomial coefficient identities, (a.k.a. terminating q-hypergeometric series.) All such identities are now routinely provable[WZ2](see below.) The machine-generated proofs of 7 and 8 appear in [ET] and [AEZ] respectively. Identities 7 and 8 immediately imply, by taking the limit , identities 7' and 8', which, in turn, are equivalent to two famous number-theoretic statements: The first Rogers-Ramanujan identity, that asserts that the number of partitions of an integer into parts that leave remainder 1 or 4 when divided by 5 equals the number of partitions of that integer into parts that differ from each other by at least 2, and Jacobi's theorem that asserts that the number of representations of an integer as a sum of 4 squares, equals 8 times the sum of its divisors that are not multiples of 4.

The WZ Proof Theory

Identities 5-8 involve sums of the form

where the summand, , is a hypergeometric term, (in 5, and 6), or a q-hypergeometric term, (in 7, and 8), in both n and k, which means that both quotients and are rational functions of ( respectively).

For such sums, and multi-sums, we have ([WZ2]) the following result.

The Fundamental Theorem of Algorithmic Hypergeometric Proof Theory:

Let be a proper (see [WZ2]) hypergeometric term in all of . Then there exist polynomials and rational functions such that satisfy

and hence, if for every specific n, has compact support in , the definite sum, , given by

satisfies the linear recurrence equation with polynomial coefficients:

follows from by summing over , and observing that all the sums on the right telescope to zero.

If the recurrence happens to be first order, i.e. L=1 above, then it can be written in closed form: for example the solution of the recurrence , , is .

This ``existence'' theorem also implies an algorithm for finding the recurrence (i.e. the ) and the accompanying certificates , see below.

An analogous theorem holds for q-hypergeometric series[WZ2][K].

Since we know how to find, and prove, the recurrence satisfied by any given hypergeometric sum or multi-sum, we have an effective way of proving any equality of two such sums, or the equality of a sum with a conjectured sequence. All we have to do is check whether both sides are solutions of the same recurrence, and match the appropriate number of initial values. Furthermore, we can also use the algorithm to find new identities. If a given sum yields a first-order recurrence, it can be solved, as mentioned above, and the sum in question turns out to be explicitly evaluable. If the recurrence obtained is of higher order, then most likely the sum is not explicitly-evaluable (in closed form), and Petkovsek's algorithm[P], that decides whether a given linear recurrence (with polynomial coefficients) has closed form solutions, can be used to find out for sure.

Almost Certainty For An Of The Cost

Consider identity once again, where is ``nice''. Dividing through by and letting (Herb Wilf's wonderful trick), we can assume that we have to prove an identity of the form

The WZ theory promises you that the left side satisfies some linear recurrence, and if the identity is indeed true, then the sequence should be a solution (in other words ). For the sake of simplicity, let's assume that the recurrence is minimal, i.e. is , (this is true anyway in the vast majority of the cases.) To prove the identity, by this method, we have to find rational functions such that the satisfy:

By dividing through by F, and clearing denominators, we get a certain functional equation for the , from which it is possible to determine their denominators . Writing , the proof boils down to finding polynomials , with coefficients that are rational functions in n and possibly other (auxiliary) parameters. It is easy to predict upper bounds for the degrees of the in . We then express each symbolically, with ``undetermined'' coefficients, and substitute into the above-mentioned functional equation. We then expand, and equate coefficients of all monomials , and get an (often huge) system of inhomogeneous linear equations with symbolic coefficients. The proof boils down to proving that this inhomogeneous system of linear equations has a solution. It is very time-consuming to solve a system of linear equations with symbolic coefficients. By plugging in specific values for n and the other parameters, if present, one gets a system with numerical coefficients, which is much faster to handle. Since it is unlikely that a random system of inhomogeneous linear equations with more equations than unknowns can be solved, the solvability of the system for a number of special values of n and the other parameters is a very good indication that the identity is indeed true. It is a waste of money to get absolute certainty, unless the conjectured identity in question is known to imply the Riemann Hypothesis.

Semi-Rigorous Mathematics

As wider classes of identities, and perhaps even other kinds of classes of theorems, become routinely-provable, we might witness many results for which we would know how to find a proof (or refutation), but we would be unable, or unwilling, to pay for finding such proofs, since ``almost certainty'' can be bought so much cheaper. I can envision an abstract of a paper, c. 2100, that reads : ``We show, in a certain precise sense, that the Goldbach conjecture is true with probability larger than , and that its complete truth could be determined with a budget of .'' It would be then OK to rely on such a priced theorem, provided that the price is stated explicitly. Whenever statement A, whose price is p, and statement B, whose price is q, are used to deduce statement C, the latter becomes a priced theorem priced at p+q.

If a whole chain of boring identities would turn out to imply an interesting one, we might be tempted to redeem all these intermediate identities, but we would not be able to buy out the whole store, and most identities would have to stay unclaimed.

As absolute truth becomes more and more expensive, we would sooner or later come to grips with the fact that few non-trivial results could be known with old-fashioned certainty. Most likely we will wind up abandoning the task of keeping track of price altogether, and complete the metamorphosis to non-rigorous mathematics. Note: Maple programs for proving hypergeometric identities are available by anonymous ftp to math.temple.edu, in directory pub/zeilberger/programs. a Mathematica implementation of the single-summation program, can be obtained from Peter Paule at paule@risc.uni-linz.ac.at .

References

[AZ] G. Almkvist and D. Zeilberger, The method of differentiating under the integral sign, J. Symbolic Computation 10(1990), 571-591.

[AEZ] G. E. Andrews, S. B. Ekhad, and D. Zeilberger A short proof of Jacobi's formula for the number of representations of an integer as a sum of four squares, Amer. Math. Monthly, 100(1993), 274-276.

[ALMSS] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy, Proof verification and intractability of approximation problems, Proc. 33rd Symp. on Foundations of Computer Science (FOCS), IEEE Computer Science Press, Los Alamitos, 1992, pp. 14-23.

[AS] S. Arora, and M. Safra, Probabilstic checking of proofs, ibid, pp. 2-13.

[Ca] P. Cartier, Démonstration ``automatique'' d'identités et fonctions hypergéometriques [d'apres D. Zeilberger], Séminaire Bourbaki, exposé 746, Astérisque 206, 41-91, SMF, 1992.

[CF] P. Cartier and D. Foata, Problèmes combinatoires de commutation et réarrangements, Lecture Notes Math. v. 85, Springer 1969.

[Ci] B. Cipra, Theoretical computer scientists develop transparent proof techniques, SIAM News, 25/3(May 1992).

[D] J. Dawson, The Gödel incompleteness theorem from a length of proof perspective, Amer. Math. Monthly 86(1979), 740-747.

[E] S. B. Ekhad, A very short proof of Dixon's theorem, J. Comb. Theo. Ser. A 54(1990), 141-142.

[ET] S. B. Ekhad and S. Tre, A purely verification proof of the first Rogers-Ramanujan identity, J. Comb. The. Ser. A 54(1990), 309-311.

[G] K. Gödel, On length of proofs, (in German) Ergeb. Math. Colloq. 7(1936), 23-24. Translated in ``The Undecidable'' (M. Davis, Ed.), Raven Press, Hewitt, NY, 1965, 82-83.

[JQ] A. Jaffe and F. Quinn, ``Theoretical mathematics'': Toward a cultural synthesis of mathematics and theoretical physics, Bulletin(N.S.) of the Amer. Math. Soc. 29(1993), 1-13.

[K] T. H. Koornwinder, Zeilberger's algorithm and its q-analogue, University of Amsterdam Mathematics department preprint.

[P] M. Petkovsek, Hypergeometric solutions of linear recurrence equations with polynomial coefficients, J. Symbolic Computation 14(1992), 243-264.

[S] J. Spencer, Short theorems with long proofs, Amer. Math. Monthly 90(1983), 365-366.

[WZ1] H. S. Wilf and D. Zeilberger, Rational functions certify combinatorial identities, J. Amer. Math. Soc. 3(1990), 147-158.

[WZ1a] ------, Towards computerized proofs of identities, Bulletin(N.S.) of the Amer. Math. Soc. 23(1990), 77-83.

[WZ2] -------, An algorithmic proof theory for hypergeometric (ordinary and ``q'') multisum/integral identities, Invent. Math. 108(1992), 575-633.

[WZ2a] ------, Rational function certification of hypergeometric multi-integral/sum/``q'' identities, Bulletin(N.S.) of the Amer. Math. Soc. 27(1992) 148-153.

[Z1] D. Zeilberger, A Holonomic systems approach to special functions identities, J. of Computational and Applied Math. 32(1990), 321-368.

[Z2]------, A Fast Algorithm for proving terminating hypergeometric identities, Discrete Math 80(1990), 207-211.

[Z3]------, The method of creative telescoping, J. Symbolic Computation 11(1991), 195-204.

[Z4]------, Closed Form (pun intended!), ``Special volume in memory of Emil Grosswald'', M. Knopp and M. Sheingorn, eds., Contemporary Mathematics 143, 579-607, AMS, Providence, 1993.

July 1993 ; Revised: August 1993.