Mathematische Beweise in der Schule konnte ich noch nie so richtig nachvollziehen. Sie wissen schon, in Mathe gab es ja schon immer das Ziel, eine aufgestellte These zu beweisen. Also etwas durch Formeln und Gleichungen wasserdicht zu belegen. Ich erinnere mich nur ungerne an die Mathe-Stunden in der Schule, bei denen es um einen Beweis ging. Heute bin ich froh, wenn ich einen Dreisatz weitgehend fehlerfrei hinbekomme. Von Beweisen ganz zu schweigen. Kurzum: ich war immer froh, einen Taschenrechner zu haben oder einen Computer.

1976 kam es dann aus Sicht einiger Mathematiker zum Super-GAU. Erstmals in der Geschichte der Zahlen und geometrischen Formen wurde eine These nicht durch Mathematiker bewiesen, sondern durch einen Computer: das Vier-Farben-Problem. Das wurde 1852 von Francis Guthrie erstmals beschrieben und besagt, dass vier Farben ausreichen, um jede beliebige Landkarte zu kolorieren, ohne dass zwei aneinandergrenzende Länder die gleiche Farbe haben. Guthrie malte Landkarten englischer Grafschaften aus und schaffte das immer mit vier Farben. Aber die Frage war: Gilt das auch für die Weltkarte? Oder für eine Karte mit den Stadtteilen Münchens, Londons, Pekings oder Greifswalds? Und überhaupt: für jede nur erdenkbar mögliche Landkarte?

Über hundert Jahre gelang es keinem Mathematiker, einen fehlerfreien Beweis zu liefern. Was nicht heißt, dass die Aussage nicht stimmt. Es bedeutet lediglich, dass noch nicht zu 100 Prozent ausgeschlossen werden kann, dass es doch irgendeine (theoretische) Landkarte gibt, bei der man fünf (oder mehr) Farben benötigt. Der Beweis, dass vier Farben immer reichen, stand noch aus. Wie gesagt, bis 1976 zumindest. Da zeigten Kenneth Appel und Wolfgang Haken von der Universität Illinois, dass es lediglich 1.936 verschiedene »Landkartentypen« gibt und eben nicht unendlich viele. Und dann ließen sie einen Computer all diese 1.936 Varianten durchrechnen und das Computerprogramm zeigte, dass für alle Fälle tatsächlich vier Farben ausreichten.

Bis heute wird dieser durch Computer berechnete Beweis des Vier-Farben-Theorems von Zahlenkünstlern kritisiert, denn es ist keine mathematische Herleitung mit Formeln und Gleichungen, sondern nichts anderes als eine Brute-Force-Attacke, bei der einfach alle möglichen Varianten durchprobiert wurden. Tatsächlich ist es ein unschöner – ja fast sogar brachialer – Akt gewesen, der die schönen Aspekte der Mathematik wie Mandelbrot-Fraktale, den goldenen Schnitt oder die Zahl Pi geradezu würdelos zerstampft.

Einer der Kritikpunkte ist die fehlende Eleganz der Lösung des Problems. Was die Kritiker zudem bemängeln, ist die Tatsache, dass man sich auf die korrekte Verarbeitung der Berechnung durch die Hardware (CPU) und die des Computerprogramms verlassen muss. Kurzum: der computergestützte mathematische Beweis ist von Menschen nicht nachvollziehbar.

Womit wir wieder beim Anfang – dem ersten Satz – dieser Kolumne wären. Ich bin nicht allein.