Published in this issue of Philosophical Transactions are the results of a two-day debate held by a group of mathematicians, computer scientists and philosophers, organized in October 2004 by the Royal Society. It contains the talks given at that meeting together with discussions, questions and comments of the participants. Here is a sample of its contents:
• Computing and the culture of proving, by D. MacKenzie
• The challenge of computer mathematics, by H. Barendregt and F. Wiedijk
• What is a proof?, by A. Bundy, M. Jamnik and A. Fugard
• Highly complex proofs and implications of such proofs, by M. Aschbacher
• Skolem and pessimism about proof in mathematics, by P.J. Cohen
• The mathematical significance of proof theory, by A. Macintyre
• The justification of mathematical statements, by P. Swinnerton-Dyer
• Pluralism in mathematics, by E.B. Davis.
Mathematical proofs rank among the highest peaks of human thought but their complexity and variety have increased continuously along the years. Until the middle of the last century it was commonplace to say that a rigorous mathematical proof consisted of a chain of logical steps whose correctness could be checked, in due time, by a person in possession of the appropriate training. Euclid´s Elements contains numerous examples and time, as was correctly stated by Hardy, has not been able to add a single wrinkle to the freshness of their beauty and precision. But the nature of proof has not been static and mathematicians have created new and more powerful strategies, involving new concepts and tools, which provide us with greater freedom and power of reasoning.
Some of these proofs involve long chains of thoughts in an indirect and complicated manner. An example is given by Carleson´s theorem about the almost everywhere convergence of the Fourier series of a square integrable function. Another is the proof obtained by A. Wiles of Fermat´s last theorem. More recently we have the solution of Poincare´s conjecture by G. Perelmann. They are good examples of rigorous proofs that need very many ingenious steps, and which are also deep, elegant and beautiful. But they are so complex that it is doubtful that there exists a single mathematician who would be able to verify the three of them in a reasonable amount of time.
A special treatment deserves the classification of finite simple groups, the proof of which is scattered in more than 10,000 pages, divided into hundred of papers written by a hundred different mathematicians. Since the probability of finding a mistake on a very long mathematical text is not negligible, we may legitimately asks about the necessity of such long and complex proofs and their reliability, particularly when taking into account the next turn of the screw: the famous birth of the so-called computer-assisted, or computed-based, proofs of the “four colour problem” and the solution of “Kepler´s conjecture”.
• Will computers in the future be able to formulate interesting conjectures and prove theorems?
• Are mathematicians an endangered species?
• Will the mathematics of tomorrow be full of proofs that depend upon calculations that can only me performed by very powerful computers?
• Has the existence of the modern computer changed mathematics into an experimental science?
• Will computers help mathematicians to successfully treat the more complex models of nature?
These are just a sample of the interesting questions that were addressed by the participants in the debate, giving ideas and opinions that are collected in this special issue of Philosophical Transactions, whose very clarifying and stimulating reading we strongly recommend.