help annotate
Contents Next: Zeilberger and the Up: Experimental Mathematics Previous: Journal of

[Annotate][Shownotes]


The major focus of this section is Imre Lakatos's description of the deductivist style in Proofs and Refutations. An extreme example of this style is given in the form of a computer generated proof of in the box.
Euclidean Methodology has developed a certain obligatory style of presentation. I shall refer to this as `deductivist style'. This style starts with a painstakingly stated list of axioms, lemmas and/or definitions. The axioms and definitions frequently look artificial and mystifyingly complicated. One is never told how these complications arose. The list of axioms and definitions is followed by the carefully worded theorems. These are loaded with heavy-going conditions; it seems impossible that anyone should ever have guessed them. The theorem is followed by the proof. ([11] p. 142)
This is the essence of what we have called formal understanding. We know that the results are true because we have gone through the crucible of the mathematical process and what remains is the essence of truth. But the insight and thought processes that led to the result are hidden.
In deductivist style, all propositions are true and all inferences valid. Mathematics is presented as an ever-increasing set of eternal, immutable truths. ([11] p. 142)
Deductivist style hides the struggle, hides the adventure. The whole story vanishes, the successive tentative formulations of the theorem in the course of the proof-procedure are doomed to oblivion while the end result is exalted into sacred infallibility. ([11] p. 142)

Perhaps the most extreme examples of the deductivist style come out of the computer generated proofs guaranteed by Wilf and Zeilberger's algorithmic proof theory. It is important to note here that Wilf and Zeilberger transform the problem of proving identities to the more computer oriented problem of solving a system of linear equations with symbolic coefficients.

These WZ proofs (see next page) are perhaps the ultimate in the deductivist tradition. At present, knowing the WZ proof of an identity amounts to little more (We will discuss the importance of certificates later.) than knowing that the identity is true. In fact, Doron Zeilberger in [15] has advocated leaving only a QED at the end of the statement, the author's seal that he has had the computer perform the calculations needed to prove the identity. The advantage of this approach is that the result is completely encapsulated. Just as one would not worry about how the computer multiplied two huge integers together or inverted a matrix, one now has results whose proofs are uninteresting.



help annotate
Contents Next: Zeilberger and the Up: Experimental Mathematics Previous: Journal of