Automatizing proofs from Aristotle to the 21st century

BLOG: Heidelberg Laureate Forum

Laureates of mathematics and computer science meet the next generation
Heidelberg Laureate Forum

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.

800px-World_map_colored_using_the_four_color_theorem_including_oceans

Given a map with clearly delineated countries. How many different colors do you need to color in each country, avoiding like-colored countries joined by a common border? As it turns out, four is enough. The proof is anything but straightforward, though. Image: Adam Iragaël via Wikimedia Commons under CC BY-SA 4.0

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.

Hoare B. Kreutzer1
Tony Hoare ©HLFF/B.Kreutzer

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.

 

Markus Pössel hatte bereits während des Physikstudiums an der Universität Hamburg gemerkt: Die Herausforderung, physikalische Themen so aufzuarbeiten und darzustellen, dass sie auch für Nichtphysiker verständlich werden, war für ihn mindestens ebenso interessant wie die eigentliche Forschungsarbeit. Nach seiner Promotion am Max-Planck-Institut für Gravitationsphysik (Albert-Einstein-Institut) in Potsdam blieb er dem Institut als "Outreach scientist" erhalten, war während des Einsteinjahres 2005 an verschiedenen Ausstellungsprojekten beteiligt und schuf das Webportal Einstein Online. Ende 2007 wechselte er für ein Jahr zum World Science Festival in New York. Seit Anfang 2009 ist er wissenschaftlicher Mitarbeiter am Max-Planck-Institut für Astronomie in Heidelberg, wo er das Haus der Astronomie leitet, ein Zentrum für astronomische Öffentlichkeits- und Bildungsarbeit. Pössel bloggt, ist Autor/Koautor mehrerer Bücher, und schreibt regelmäßig für die Zeitschrift Sterne und Weltraum.

Leave a Reply


E-Mail-Benachrichtigung bei weiteren Kommentaren.
-- Auch möglich: Abo ohne Kommentar. +