Automatizing proofs from Aristotle to the 21st century
While (or because?) both in general laureate attendance and number of lectures, computer science certainly has greater volume than mathematics at this year’s Heidelberg Laureate Forum, it was interesting to see that there were quite a few talks connecting the foundations of computer science to mathematics.
Tony Hoare’s Tuesday lecture went farthest into the past to make the connection. Hoare traced the antecedents of computer science back to Aristotle’s logic, and identified the separation of the structure of a proof from its subject matter as the key step towards a development where today’s computer science comes to the aid of pure mathematics: If all Greeks are human beings, and all human beings are mortal, then all Greeks are mortal, and the structure of the proof can be formulated in a general way that knows nothing about Greeks, human beings or mortality.
A late descendant of this development are generic computer-based methods of proof. The adjective “generic” is important, since mathematicians, with good reason, do not readily trust customized, voluminous computer programs used for mathematical proofs. A case in point is the four-color theorem(cf. image), first proved in 1976 bei Kenneth Appel and Wolfgang Haken using a custom computer program. But in order to check such a customized computer-based proof, you need to go through the program line by line, understanding what is happening. Usually, this is fairly difficult – and sometimes it is, in practice, impossible.
Consider, more recently, the formal proof for Kepler’s conjecture on the optimal way of stacking spheres (such as oranges) in a large crate. The first computer-based proof, by Thomas Hales in 1999, consisted not only of 250 pages of notes, but also of 3 GB of computer programs and data. When it was submitted for publication, the only statement a twelve-referee panel could make after having studied the material for four years was that they were 99% certain of the correctness of the proof, which is scant comfort for mathematicians.
That is why general-purpose proof checking software is so important. Such software is the embodiment of Aristotle’s separation of logic and subject. The software does not need to know about colors, or areas, or boundaries, let alone oranges. But once the proof is written down, it can check whether the various steps follow from each other in a logical way. And once the proof-checking software has been verified by mathematicians – a much easier task not only because of the limited length of the program – it can be applied to a variety of different proofs.
In 2005, Georges Gonthier published a formal proof of the four color theorem, using the general-purpose proof assistant Coq, which incidentally featured several times in various HLF talks. Score another one for Aristotle’s method of separating the validity-checking of the proof from the subject matter! And Thomas Hales, clearly not content with getting only 99 out of 100 from the review panel, published a formal proof, using general-purpose proof-checking software, in January 2015.
So while the computer science laureates outnumber the mathematicians almost 2 to 1 in this year’s HLF, fundamental mathematics is well-represented – thanks to the connections between the two subjects, which can be traced back to Aristotle.
As always, Hoare’s HLF lecture is also online and can be viewed here.