Automatisierte Beweise von Aristoteles bis heute

BLOG: Heidelberg Laureate Forum

Laureates of mathematics and computer science meet the next generation
Heidelberg Laureate Forum
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

Gerade weil die Informatik-Laureaten beim HLF in der klaren Mehrheit sind, war es interessant zu sehen, welche große Rolle die reine Mathematik in den bisherigen HLF-Vorträgen gespielt hat – über die zum Teil sehr tiefreichenden Verbindungen der beiden Fächer.

Der Vortrag von Tony Hoare am Dienstag ist dabei sicherlich am weitesten in die Vergangenheit vorgestoßen. Hoare hat die Vorläufer der Informatik bis zurück zur Logik des Aristoteles verfolgt. Der damalige Schlüsselschritt: Die Trennung zwischen der Form des Beweises und dem Inhalt seiner Aussagen. Wenn alle Griechen Menschen sind und alle Menschen sterblich, dann sind eben auch alle Griechen sterblich – und der Beweis lässt sich in einer allgemeinen Form formulieren, die weder etwas von Griechen noch von Menschen und Sterblichkeit weiß.

Die modernen Abkömmlinge dieser Aufteilung betreffen einen Bereich, in dem die Informatik der Mathematik gehörig unter die Arme greifen kann: die Entwicklung generischer computergestützter Beweise. Das Adjektiv “generisch” ist dabei entscheidend. Gegenüber maßgeschneiderten computergestützten Beweisen haben Mathematiker ein gesundes Misstrauen – solche Beweise nutzen typischerweise umfangreiche Computerprogramme, und deren Richtigkeit nachzuprüfen, Zeile für Zeile, kann sich als schwierig bis praktisch unmöglich herausstellen.

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

Ein solcher Beweis betrifft das sogenannte Vierfarbentheorem (siehe Abbildung). Es wurde erstmals 1976 von Kenneth Appel und Wolfgang Haken mithilfe eines maßgeschneiderten Computerprogramms bewiesen. Ein jüngerer Fall ist die Kepler’sche Vermutung, bei der es um das optimale Verfahren geht, gleichgroße Kugeln wie z.B. Orangen in eine große Kiste zu packen. Der erste computergestützte Beweis der Vermutung, vorgelegt von Thomas Hales im Jahre 1999, bestand aus 250 Seiten von Notizen plus 3 Gigabyte an Computercode und Daten. Nachdem der Beweis zur Veröffentlichung eingereicht worden war, konnte ein zwölfköpfiges Team von Gutachtern nach vier Jahren Auseinandersetzung mit dem Material nichts weiter sagen, als dass sie zu 99% sicher wären, dass der Beweis stimmen würde. Keine sehr beruhigende Aussage für Mathematiker.

Deswegen ist generische Beweisprüfungs-Software so wichtig – als moderne Form von Aristoteles Trennung von Struktur und Inhalt eines Beweises. Solche Software weiß nichts von Farben, Flächen, Grenzen oder Orangen. Aber sobald ein Beweis in der richtigen Form aufgeschrieben ist, kann die Software prüfen, ob die Beweisschritte logisch aufeinander aufbauen. Und sobald die Software ihrerseits einmal von Mathematikern geprüft und für korrekt befunden ist, kann man sie auf eine Vielzahl verschiedener Beweise anwenden.

Im Jahre 2005 veröffentlichte Georges Gonthier einen Beweis der Vierfarben-Theorems, der die generische Beweisprüfungssoftware Coq nutzte – nebenbei bemerkt: diese Software kam gleich in einer ganzen Reihe von HLF-Vorträgen vor. Ein später Erfolg für Aristoteles und sein Trennungsverfahren! Auch Thomas Hales war mit den 99%, die ihm bescheinigt worden waren, offenbar unzufrieden. Im Januar dieses Jahres veröffentlichte er einen Beweis für die Kepler’sche Vermutung, der ebenfalls generische Beweisprüfungs-Software nutzte.

Unter anderem in dieser Weise ist die reine Mathematik beim diesjährigen HLF gut vertreten – dank tiefer Verbindungen zwischen den beiden Fächern, die sich aus unseren Tagen bis zu Aristoteles zurückverfolgen lassen.

Wie alle HLF-Vorträge ist auch der von Hoare online und kann hier angeschaut werden.

Avatar photo

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.

1 comment

  1. Autsch! Die Weltkarte zur Illustration des Vierfarbensatzes ist mathematisch unsinnig!

    Denn der Satz setzt voraus, dass alle Länder aus einem zusammenhängenden Gebiet bestehen. (Sonst kann man leicht Karten konstruieren, die sich nicht mit vier Farben färben lassen, jedenfalls wenn alle Gebiete eines Landes die gleiche Farbe haben sollen.) Leider gibt es Staaten in der Welt, die aus mehreren nicht-zusammenhängenden Gebieten bestehen. Deutlich sichtbar auf der Weltkarte: Die ältesten 48 Staaten der USA und Alaska hängen nicht zusammen.

    Die Vierfärbbarkeit der Weltkarte folgt nicht aus dem Vierfarbensatz. Sie ist reiner Zufall.

Leave a Reply


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