You are here

Computation, Proof, Machine

Gilles Dowek
Cambridge University Press
Publication Date: 
Number of Pages: 
[Reviewed by
Allen Stenger
, on

This is a popular-science book (although an abstruse one) about the role of computation in mathematical proof. “Computation” is used here very broadly, and encompasses not only numerical calculation but any kind of algorithm than can be carried out without human judgment, such as a computer program. The book starts with the ancient Mesopotamians, and has a lot about predicate calculus, Church’s lambda-calculus, and the decision problem, but is really aimed at automated proofs (such as the computer part of the Appel–Haken proof of the four color theorem) and automated checking of proofs. The present book is a 2015 translation of the 2007 French-language book Les Métamorphoses du calcul. Une étonnante histoire de mathématiques.

The Appel–Haken proof in 1976 is the one everyone has heard of, but the author points out that since then several more long computer-aided proofs have been discovered, such as the 1998 proof by Hales of Kepler’s conjecture on sphere packing. The author also points out that some computer proofs go almost back to the beginning of computers, such as proofs that certain very large numbers are prime or that the digits of \(\pi\) are as stated.

On p. 31 we read that the heart of the book is “the metamorphoses of computation in the twentieth century.” The author contends in the last section of the book that the Appel–Haken proof has introduced a “methodological revolution” (p. 116) and precipitated a “crisis of the axiomatic method” (pp. 87 ff). This crisis is not defined explicitly but is tied to his belief that axioms should be replaced by computation rules. Usually these rules say the same thing in more active language; for example (p. 135) instead of the axiom \(x + 0 = x\) we have have a rule that \(x + 0\) can be replaced by \(x\).

The author analyzes some of the objections to computer proofs. One is that we feel that a problem with a short statement (such as the four-color theorem) should have a short proof, while one with a long statement (such as that a million-digit number is prime) cannot be expected to have a short proof. Another is that computer proofs are not “explicative” (pp. 117–119); that is, they show that the result is true but do not explain why it is true. The author thinks the verifying role of proofs needs to be separated from the explicative role. (The author doesn’t mention this, but lots of hand proofs are not explicative either, such as ones that begin “Consider the following [long and mysterious] expression.” Most proofs by induction are not explicative.)

I think the “crisis” and “revolution” parts of the book are overstated; the automated work such as the Apple–Haken theorem have generated a lot of buzz, but have almost no effect on the mathematician’s day-to-day work. The author’s special interest is automated proof checking rather than automated proving, and the latter portions of the book are slanted in that direction. He does not mention a couple of automated areas that really are potentially revolutionary. The methods of hypergeometric summation due to Wilf & Zeilberger and others have revolutionized this special subfield of mathematics; problems that were previously almost impossible can now be done completely by the computer, which will even print out a short proof of the result’s correctness for you. Experimental mathematics is a rapidly-growing field, popularized by Jonathan Borwein and others, and making it possible to guess the value of a sum or integral by calculating its numerical value to a high precision (you still have to invent your own hand proof once you have guessed the value).

Very Bad Feature: no index. It is a short book, but it uses a lot of specialized terminology and it’s important to understand exactly what the term means in order to follow the argument.

Bottom line: an interesting but frustrating book that spans wide areas of philosophy, logic, foundations of mathematics, and computer science.

Allen Stenger is a math hobbyist and retired software developer. He is an editor of the Missouri Journal of Mathematical Sciences. His mathematical interests are number theory and classical analysis.

Part I. Ancient Origins:
1. From the prehistory to the Greeks
2. Two thousand years of computation
Part II. The Age of Reason:
3. Predicate logic
4. The decision problem
5. Church's thesis
6. Lambda-calculus
7. Constructivity
8. Constructive proofs and algorithms
Part III. Crisis of the Axiomatic Method:
9. Intuitionistic type theory
10. Automated proof
11. Automated proof checking
12. News from the field
13. Instruments
14. The end of axioms?
15. Conclusion: as we near the end of this mathematical voyage.