There is an article by
Marcus du Sautoy entitled
Burden of Proof in this week's New Scientist, which discusses the issue of whether a computer generated mathematical proof can be considered to actually be a proof, especially since some such proofs are so lengthy that they cannot be checked by a human. An example of this type of proof is the
4-colour map theorem.
My own view on this issue is that a computer generated proof has
exactly the same status as a human generated proof. The difference is only one of the degree of assistance provided to the brain of the human to help with the generation of the proof. A totally unassisted human would have to somehow do the whole proof mentally, which severely limits the length of proofs that are accessible. A human with the typical assistance that is allowed in an examination room (i.e. pen and paper) has the luxury of at least being able to write things down, which allows
much longer proofs to be reliably generated. The mechanics of generating a proof then reduce to using well-defined rules to manipulate symbolic expressions, where pen and paper are used as a medium for representing these symbols, and the rules are implemented in the human brain.
The degree of assistence in generating a proof can be taken one stage further by using a computer to implement some or all of the rules for manipulating the symbolic expressions, rather than implementing all of the rules in the human brain. This seems to be a fairly radical step to take, because hitherto the only part of the proof that was "outside" the human brain was its "dumb" representation using pen and paper, whereas the "clever" bit involving the implementation of rules to manipulate this representation was "inside" the human brain.
Let us consider what these rules of manipulation actually are. Effectively, they define a procedure for taking an initial expression constructed out of symbols, and repeatedly operating on it using the rules to eventually generate the required final expression. The cleverness is in the
construction of the set of rules, which is where a human is the best source of the cleverness needed to create the rules. There is
no cleverness in the repeated
application of these rules; all that is required is that their application is done
reliably, which is where a computer is the best approach, especially if the proof has many steps.
Use a human to
define the rules of manipulation, and use a computer to
implement these rules. This approach seems to me to be entirely uncontroversial, and it is exactly how computer generated proofs are done. Note that software bugs in the computer part of the proof are dealt with in an
analogous way to "software" bugs in human part of the proof, i.e. try a variety of approaches on a variety of platforms.
Interestingly, I wrote a paper (see
here)
Luttrell S P, 1999, Self-organised modular neural networks for encoding data, in Combining Artificial Neural Networks: Ensemble and Modular Multi-Net Systems (Perspectives in Neural Computing, Springer-Verlag, ed. Sharkey A J C), pp. 235-263
in which I used a computer (running the symbolic algebra program
Mathematica) to help me derive some results on the optimisation of vector quantisers so that their Euclidean distortion was minimised, and this optimisation was done
non-parametrically in order to discover the globally optimal solution. The only way that I have found to do this type of optimisation involves intermediate expressions that can have a
large number of terms, but which eventually leads to results that can be quite
compact, and which are thus interesting. The only sensible way of handling this type of derivation is to automate it using a computer to implement the rules of manipulation (i.e. using symbolic algebra). As far as I can tell other people have
not taken up my idea of using symbolic algebra to derive this type of result; my paper went down like a lead balloon, which is a great pity.
Update: OK, I can see that the
Mathematica notebook in which I derive the results that I published in the above paper (see
here) has now been downloaded 22 times (as of 31 December 2006). It would be interesting to hear your comments on it. Maybe you think it is just a load of algebraic twiddling which is not much use in the real world, but that conclusion would ignore the fact that
exact algebraic solutions to toy problems are a powerful source of insight for interpreting
approximate numerical solutions to real world problems.