Obviously, the value of a computer assisted proof is that we know the result is true! We cannot build on a theorem until we know it has been verified. In order for mathematics to go forward, we need to use all the tools we have; sometimes that means we need to rely on computer assisted proofs. So be it.
Some mathematicians have tried to protect their egos by proposing that human proofs are superior to computer assisted proofs. They claim that we don't learn as much from computer assisted proofs as we do from a human proofs. They claim computer proofs can be difficult to verify. They claim computer proofs are less elegant. I find these complaints to be naive.
In my opinion, computer assisted proofs are revolutionary mathematics. Every new computer assisted proof is another example which we can learn from. This is a brand new technique in the history of mathematics. We weren't born knowing how to apply induction and we weren't born knowing how to construct a proper computer assisted proof. We need to see a wide variety of examples before we are comfortable using this technique. We need to know the scope of problems which are amenable to computer assistance. We need to read clearly written arguments and algorithms which prove theorems via this new method in order to appreciate their elegance and set standards for publication.
All computer assisted proofs need to be written up properly in order to gain acceptance. The computer portion of the proof should include a well documented algorithm that can be implemented in any computer language and in any operating system. Having multiple implementations by different people gives the reader confidence that the implementation is correct just like having multiple referees for a journal article gives the reader confidence. Journals can't publish much computer code, but it is easy to make code available on a web site. The code for a computer assisted proof should be well documented and CAREFULLY TESTED. High standards for testing code in computer assisted proofs cannot be underestimated.
What types of theorems are amenable to computer assisted proofs? That is hard to say at this time. I am amazed at the array of results that have been given computer proofs. For example, Hales proof of the Kepler conjecture is a real victory because it is very difficult to determine a transcendental number by computer where there is always an issue with roundoff error. The WZ-Method for proving identities on hypergeometric series is beautifully described in the book A=B by Petkovsek, Wilf and Zeilberger. The latest proof of the 4 Color Theorem by Robertson, Sanders, Seymour and Thomas is a perfect example of a well written computer assisted proof; the written portion of the proof is about 18 pages, the computer code generates the entire reducible/unavoidable set itself so no human input of graphs is required, the code has been implemented by multiple people in multiple languages. As a final example of computer assisted proofs, Postnikov and I have shown that smooth Schubert varieties for all flag manifolds G/B with G being a simple complex Lie group can be characterized efficiently using generalized pattern avoidance.
What else can be learned from a computer proof? Well, every computer proof I have read contains some miracle that makes it feasible to check by computer. For example, it is absolutely a miracle that the 4 color theorem can be proved by computer because it could have been the case that every reducible/unavoidable set has size at least 10^50, but no, somehow the Robertson, Sanders, Seymour, Thomas algorithm found a reducible unavoidable set with only 631 elements. That's nothing for a computer! These miracles are not stand alone theorems, but they are lemmas in our usual hierarchy of lemmas, propositions, and theorems. They tell us something about the complexity of the objects we are working with. They add to our intuition and perspective on the mathematics.
At many conferences and seminars, we have all heard someone announce the first ``geometrical proof of a theorem due to so-and-so'', or the first ``purely combinatorial proof'' or the first ``algebraic proof'', etc. Proving theorems using different tools is very useful because it helps connect the work to other areas of mathematics, it can make the proof accessible to a wider audience, and it encourages the discovery of new tools. However, we don't often hear people speaking about the first ``computer assisted proof'' of any known result. Computer proofs are scorned by many mathematicians; they are the proof given only when no ``human'' proof is known. It is a mistake to scorn the most useful invention mathematics has seen since the pencil.
I want to challenge you to consider trying to prove some result by computer as soon as possible in order to practice the technique. Computer proof techniques are in their infant phase today. They are not taught in the same way that we teach other methods of proof such as induction, proof by contradiction, or proof by contrapositive. We have only heuristic methods for even recognizing when a theorem is amenable to a computer proof in most fields. We must develop our skills at computer proving so that we can take advantage of this amazing invention when the need arises. We must explore the road toward a good computer proof because it will lead to new mathematics. We must set standards for publication of computer assisted proofs when the journal cannot include all of the code. We must encourage mathematicians whose pioneering research embraces this new approach and provides us with more examples to learn from. To encourage exploration in the area of computer assisted proof, I ask "Is there a slick computer assisted proof of Fermat's last theorem?"
If others would like to contribute to the prize, I will start taking up a collection.
View this page in Romanian courtesy of azoft