Die Mathematik ist die Königin der Wissenschaften. Ihre strengen Gewissheiten bezieht sie aus rein formalen Schlussfolgerungen, nicht aus empirischen Beobachtungen. Die "exakten" Wissenschaften dürfen sich nur so nennen, weil sie sich bei ihren Aussagen über die Natur mathematischer Sprache bedienen. Insofern beruht der Gültigkeitsanspruch der Naturwissenschaft nicht nur auf der Prüfbarkeit durch das Experiment, sondern auch auf der unerschütterlichen Zuverlässigkeit mathematischer Sätze.

Das felsenfeste Vertrauen in die Königin der Wissenschaften gerät freilich ein wenig ins Wanken, wenn – wie jüngst gemeldet – ein rundes Dutzend Gutachter nach vier Jahre langer Prüfung eines mathematischen Beweises am Ende mitteilt, man sei von dessen Richtigkeit ziemlich überzeugt, habe nun aber einfach keine Energie mehr, dies mit hundertprozentiger Sicherheit zu attestieren (Nature, Bd. 424, S. 12).

Bei dem skurrilen Fall geht es um ei-ne Frage von trügerischer Einfachheit: Welches ist die dichteste Kugelpackung? Praktisch löst das Problem jeder Obsthändler, wenn er runde Früchte zu Pyramiden stapelt, aber schon Johannes Kepler (1571-1630) biss sich an dem Beweis, das sei die optimale Anordnung, die mathematischen Zähne aus. Der Haken ist: Es gibt zwar lokal noch dichtere Packungen, doch führen sie anderswo zu größeren Lücken.

Ende der 1980er Jahre nahm Thomas Hales – heute an der Universität Pittsburgh (Pennsylvania) – einen neuen Anlauf. Zunächst fand er heraus, dass es "nur" rund 5000 Kandidaten für die dichteste Packung gibt; um unter ihnen den Sieger zu ermitteln, musste er mehr als 100000 Ungleichungen ausrechnen. Das beschäftigte ihn selbst mit massiver Computerhilfe zehn Jahre lang. Im Sommer 1998 gab Hales schließlich bekannt, er habe die Kepler'sche Vermutung bewiesen (Spektrum der Wissenschaft 4/1999, S. 10).

Doch das Peer-Review-Verfahren der "Annals of Mathematics" ist nun nach vier Jahren an der Erschöpfung der zwölf Gutachter gescheitert. Hales wirbt seither im Internet für sein Projekt "Flyspeck" (www.math.pitt.edu/~thales/flyspeck/). Der Name bedeutet "Fliegendreck", aber auch "bis ins kleinste Detail prüfen"; außerdem enthält er die Anfangsbuchstaben von "formal proof of Kepler". Unter einem solchen formalen Beweis versteht Hales ein Computerprogramm, das sich im Gegensatz zu einem "traditionellen mathematischen Beweis" nicht auf menschliche Intuition berufen soll und darum weniger anfällig für logische Fehler sei.

Man sieht, wie Hales hier den Spieß umkehrt. Während die gutachtenden Mathematiker vor seinem computergestützten Beweis erschöpft die Waffen streckten und damit implizit zu verstehen gaben, das für sie Menschenmögliche bilde zugleich eine Grenze des mathematisch Prüfbaren, transferiert Hales das Ideal mathematischer Vollkommenheit vom menschlichen Denken auf den unermüdlichen Computer. Am Fluchtpunkt dieser Perspektive steht eine Mathematik, die in vom Menschen bedienten Rechenmaschinen stattfindet: Der Mathematiker formuliert das Problem als Programm, der Computer berechnet Resultate, die der Mensch als Output empfängt.

Hales nennt konsequenterweise als Ziel seines Flyspeck-Projekts die in Computersprache formulierte Aussage: "Die Kepler‘sche Vermutung ist wahr." Letztlich wüsste allerdings nur der Computer, warum. Durchaus denkbar, dass ein Teil der Mathematik sich in diese Richtung weiterentwickelt. Dann wird eine eigene Hilfsdisziplin entstehen, die sich darauf spezialisiert, einen vom Computer geführten Beweis derart zu interpretieren, dass menschliche Mathematiker ihm halbwegs folgen können.

Aus: Spektrum der Wissenschaft 9 / 2003, Seite 13
© Spektrum der Wissenschaft Verlagsgesellschaft mbH