(Cross-posted at
M-Phi)
Mathematics has been much in the news recently, especially with the announcement of the latest four Fields medalists (I am particularly pleased to see the first woman, and the first Latin-American, receiving the highest recognition in mathematics). But there was another remarkable recent event in the world of mathematics: Thomas Hales has announced the completion of the formalization of his proof of the Kepler conjecture. The conjecture: “what is the best way to stack a collection of spherical objects, such as a display of oranges for sale? In 1611 Johannes Kepler suggested that a pyramid arrangement was the most efficient, but couldn't prove it.” (New Scientist)
We are pleased to announce the completion of the Flyspeck project, which has constructed a formal proof of the Kepler conjecture. The Kepler conjecture asserts that no packing of congruent balls in Euclidean 3-space has density greater than the face-centered cubic packing. It is the oldest problem in discrete geometry. The proof of the Kepler conjecture was first obtained by Ferguson and Hales in 1998. The proof relies on about 300 pages of text and on a large number of computer calculations.
The formalization project covers both the text portion of the proof and the computer calculations. The blueprint for the project appears in the book "Dense Sphere Packings," published by Cambridge University Press. The formal proof takes the same general approach as the original proof, with modifications in the geometric partition of space that have been suggested by Marchal.
So far, nothing very new, philosophically speaking. Computer-assisted proofs (both at the level of formulation and at the level of verification) have attracted the interest of a number of philosophers in recent times (here’s
a recent paper by John Symons and Jack Horner, and here is
an older paper by Mark McEvoy, which I commented on at a conference back in 2005; there are many other papers on this topic by philosophers). More generally, the question of the extent to which mathematical reasoning can be purely ‘mechanical’ remains a lively topic of philosophical discussion (here’s a
1994 paper by Wilfried Sieg on this topic that I like a lot). Moreover, this particular proof of the Kepler conjecture does not add anything substantially new (philosophically) to the practice of computer-verifying proofs (while being quite a feat mathematically!). It is rather something Hales said to the
New Scientist that caught my attention (against the background of the 4 years and 12 referees it took to human-check the proof for errors): "This technology cuts the mathematical referees out of the verification process," says Hales. "Their opinion about the correctness of the proof no longer matters."
Now, I’m with Hales that ‘software intensive mathematics’ (to borrow Symons and Horner’s terminology) is of great help to offload some of the more tedious parts of mathematical practice such as proof-checking. But there are a number of reasons that suggest to me that Hales’ ‘optimism’ is a bit excessive, in particular with respect to the allegedly expendable role of the human referee (broadly construed) in mathematical practice, even if only for the verification process.
Indeed, and as I’ve been arguing in a
number of posts, proof-checking is a major aspect of mathematical practice, basically corresponding to the role I attribute to the fictitious character ‘opponent’ in my dialogical conception of proof (see
here). The main point is the issue of epistemic trust and objectivity: to be valid, a proof has to be ‘replicable’ by anyone with the relevant level of competence. This is why probabilistic proofs are still thought to be philosophically suspicious (as argued for example by
Kenny Easwaran in terms of the notion of ‘transferability’). And so, automated proof-checking will most likely never replace completely human proof-checking, if nothing else because the automated proof-checkers themselves must be kept ‘in check’ (lame pun, I know). (Though I am happy to grant that the role of opponent can be at least partially played by computers, and that our degree of certainty in the correctness of Hales’ proof has been increased by its computer-verification.)
Moreover, mathematics remains a human activity, and mathematical proofs essentially involve epistemic and pragmatic notions such as explanation and persuasion, which cannot be taken over by purely automated proof-checking. (Which does not mean that the burden of verification cannot be at least partially transferred to automata!) In effect, a good proof is not only one that shows that the conclusion is true, but also why the conclusion is true, and this explanatory component is not obviously captured by automata. In other words, a proof may be deemed correct by computer-checking, and yet fail to be persuasive in the sense of having true explanatory value. (Recall that
Smale’s proof of the possibility of sphere eversion was viewed with a certain amount of suspicion until
models of actual processes of eversion were discovered.)
Finally, turning an ‘ordinary’ mathematical proof* into something that can be computer-checked is itself a highly theoretical, non-trivial, and essentially informal endeavor that must itself receive a ‘seal of approval’ from the mathematical community. While mathematicians
hardly ever disagree on whether a given proof is or is not valid once it is properly scrutinized, there can be (and has been, as once vividly described to me by
Jesse Alama) substantive disagreement on whether a given formalized version of a proof is indeed an adequate formalization of that particular proof. (This is also related to thorny issues in the metaphysics of proofs, e.g. criteria of individuation for proofs, which I will leave aside for now.)
A particular informal proof can only be said to have been computer-verified if the formal counterpart in question really is (deemed to be) sufficiently similar to the original proof. (Again, the formalized proof may have the same conclusion as the original informal proof, in which case we may agree that the theorem they both purport to prove is true, but this is no guarantee that the original informal proof itself is valid.
There are many invalid proofs of true statements.) Now, evaluating whether a particular informal proof is accurately rendered in a given formalized form is not a task that can be delegated to a computer (precisely because one of the relata of the comparison is itself an informal construct), and for this task the human referee remains indispensable.
And so, I conclude that, pace Hales, the human mathematical referee is not going to be completely cut out of the verification process any time soon. Nevertheless, it is a welcome (though not entirely new) development that computers can increasingly share the burden of some of the more tedious aspects of mathematical practice: it’s a matter of teamwork rather than the total replacement of a particular approach to proof-verification by another (which may well be what Hales meant in the first place).
—————————–
* In some research programs, mathematical proofs are written directly in computer-verifiable form, such as in the newly created research program of
homotopy type-theory.
New APPS 
Leave a reply to Eric Schliesser Cancel reply