Mathematische Beweise Der weite Weg zur absoluten Gewissheit
Formeln an Tafel (Archivbild)
Foto: Getty Images/iStockphotoMathematiker sind zweifellos privilegiert: Im Unterschied zu allen anderen Menschen können sie von sich behaupten, Dinge mit absoluter Sicherheit zu wissen. Gut, einige Religionsführer, Politiker und Kneipengänger meinen das auch - doch in Wirklichkeit bewegen sie sich meist doch eher im Bereich des Glaubens.
In der Mathematik ist es dagegen ziemlich einfach, Gewissheit zu erlangen: Wenn ein Beweis für eine Behauptung existiert, ist kein Zweifel mehr möglich. Ein Beweis selbst ist eine streng logisch aufgebaute Argumentationskette. Er nutzt bekanntes Wissen, also auch ältere Beweise, um die Gültigkeit einer Aussage zu belegen.
Doch der hohe Anspruch an eine streng logische, lückenlose Argumentation, den die Mathematik an sich stellt, wird nur selten so erfüllt, wie man es vielleicht erwarten würde. Nur in wenigen Fällen beruht ein Beweis lediglich auf wenigen allgemein anerkannten Grundlagen, den Axiomen. Axiome legen die mathematische Basis fest - etwa was eine natürliche und was eine gebrochene Zahl ist.
Mathematiker: Sind sie besondere Menschen?
Als Beweis gilt unter Mathematikern meist einfach nur eine Argumentation, die andere Mathematiker überzeugt. Viele Vorkenntnisse werden vorausgesetzt, etwa Arbeiten von Kollegen zu dem Thema. "Ein mathematischer Beweis ist bis zu einem gewissen Punkt eher eine soziale Konvention", meint Hans Munthe-Kaas von der Universität Bergen.
Doch es gibt Mathematiker, die sich damit nicht zufrieden geben. Ihr Ziel ist, wenn man so will, die absolute Gewissheit - belegt durch eine spezielle Software, die Beweise auf ihre logische Konsistenz prüft - auch Proof Checker genannt.
Derzeit läuft ein solches Projekt an der Jacobs University Bremen. Schüler und Mathe- Studenten wollen dabei einen fast 50 Jahre alten Beweis so neu aufschreiben, dass ihn eine spezielle Software quasi verstehen und als richtig bestätigen kann. Es geht um eine unter Mathematikern sehr berühmte Aufgabe: das zehnte Hilbertsche Problem.
Gibt es ganzzahlige Lösungen oder nicht?
Der deutsche Mathematiker David Hilbert hatte 1900 auf einem Kongress eine Liste von gleich 23 offenen Fragen der Mathematik vorgelegt, die die Mathematik des 20. Jahrhunderts wesentlich beeinflusst haben. Beim Problem Nummer zehn ging es um die Frage, ob man mit Sicherheit herausfinden kann, ob bestimmte, sogenannte Diophantische Gleichungen , eine ganzzahlige Lösung haben oder nicht. Diophantische Gleichungen sind Polynome wie ax2 + by4 + c = 0, wobei die Koeffizienten a, b, c sämtlich ganzzahlig sind.
Ein Beispiel: Dass die Gleichung x2 + y4 + 1 = 0 keine ganzzahlige Lösung für x, y hat, sieht man selbst mit überschaubarem mathematischem Sachverstand recht schnell. x2 und y4 sind beides Quadratzahlen und daher größer oder gleich Null. Wenn man dazu noch 1 addiert, kann das Ergebnis nicht Null lauten.
Doch es gibt auch schwierigere diophantische Gleichungen, bei denen sich spontan kaum entscheiden lässt, ob es ganzzahlige Lösungen gibt. Für die einfache Gleichung x3 + y3 + z3 = 33 ist das beispielsweise bis heute nicht bekannt.
Es dauerte 70 Jahre, bis der russische Mathematiker Jurij Matijassewitsch das zehnte Hilbert-Problem gelöst hatte. Laut seinem Beweis aus dem Jahr 1970 existiert keine allgemeingültige Methode, um festzustellen, ob es eine ganzzahlige Lösung gibt oder nicht.
"Wir haben mit Matijassewitsch vorab über das Projekt gesprochen", sagt Dierk Schleicher von der Jacobs University. Der renommierte Mathematiker aus Sankt Petersburg unterstütze das Vorhaben. Sein Beweis ist auch als Buch erschienen und umfasst immerhin 288 Seiten.
Die Bremer Mathematiker kommen nach eigener Aussage gut voran bei der Verifizierung. "Wir haben große Teile schon mit der Software 'Isabelle' überprüft, bislang war alles korrekt", berichtet Bachelorstudent Malte Haßler. Das Projekt kam bei "Jugend forscht" auf den dritten Platz und bekam einen Sonderpreis des Bundespräsidenten .
Noch sind die Schüler und Studenten freilich nicht ganz fertig: Sie müssen noch einen wichtigen Teil des Beweises für den sogenannten Proof Checker lesbar machen. Der Beweis sieht dann auf den ersten Blick aus wie Programmiercode.
Unter Mathematikern ist die Arbeit mit Proof Checkern bislang kaum üblich. James Maynard von der Oxford University hält das auch für sinnvoll: "Es geht darum, mathematische Ideen zu verstehen." Bei jedem Beweis immer wieder bei Adam und Eva anzufangen, hält der Zahlentheoretiker für kaum praktikabel. "Der Aufwand, Beweise in formaler Sprache aufzuschreiben, ist sehr hoch."
Die Arbeit mit Proof Checkern ist äußerst umständlich, allerdings haben sie den Vorteil, dass sie kleinste Fehler in der logischen Argumentation gnadenlos aufdecken. Mathematikern ist nämlich durchaus bewusst, dass so mancher Beweis noch den einen oder anderen Schwachpunkt haben könnte. Doch dass es sich dabei um ein wirklich großes Problem handelt und wichtige Arbeiten fragwürdig sind - so weit würde kaum jemand gehen.
Stimmt wirklich alles?
"Klar, es gibt Theoreme, die veröffentlicht sind und deren Beweise Fehler haben", meint etwa Stanislaw Smirnow, russischer Gewinner der Fields-Medaille im Jahr 2010. Aber das betreffe eher nicht die großen, wichtigen Beweise. "Wenn da Fehler drin sind, werden sie über kurz oder lang gefunden."
Bjorn Poonen, Zahlentheoretiker am MIT, stimmt Smirnow zu. Die wichtigsten Beweise seien intensiv geprüft worden, nicht von Software, sondern von vielen Mathematikern. "Daher können wir guten Gewissens davon ausgehen, dass sie stimmen."
In Einzelfällen mussten Mathematiker aber auch schon Proof Checker bemühen, um Kollegen von der Richtigkeit ihrer Arbeiten zu überzeugen. Das bekannteste Beispiel für eine solche Beweisprüfung am Computer ist der berühmte Vier-Farben-Satz . Er besagt, dass man die Länder auf einer beliebigen Landkarte stets so mit vier verschiedenen Farben färben kann, dass nirgends zwei gleichfarbige Länder aneinandergrenzen.
Keplers Problem
Der Beweis selbst wurde mit Computerhilfe geführt, was viele Mathematiker nicht so recht überzeugte. 2005 jedoch konnten zwei Mathematiker mithilfe eines Proof Checkers zeigen, dass der ursprüngliche Computerbeweis des Vier-Farben-Satzes korrekt - also logisch konsistent aufgebaut ist.
Ähnlich war der US-Mathematiker Thomas Hales vorgegangen, der zunächst 1998 mit Computerhilfe die Keplersche Vermutung bewiesen hatte, in der es um das bestmögliche Aufschichten von Kugeln geht. 16 Jahre später gelang ihm dann die Überprüfung dieses Beweises mit einer dafür konzipierten Software.
Womöglich müssen Mathematiker eines Tages ihre Beweise ja stets inklusive einer Version publizieren, die ein Proof Checker verarbeiten kann. Dann hätte man quasi auf Knopfdruck die Sicherheit, dass die Argumentation fehlerfrei ist. "Bis dahin ist es aber noch ein weiter Weg", sagt MIT-Forscher Bjorn Poonen. Es sei einfach sehr aufwendig, einen mathematischen Beweis in die formale Sprache zu übersetzen, die ein Proof Checker verstehe.
Der Zahlentheoretiker bezweifelt sogar, ob das wirklich ein erstrebenswertes Ziel ist. "In jedem Fall wären das dann sehr, sehr lange Beweise, die für Menschen praktisch nicht lesbar seien", sagt er. "Ein Beweis sollte aber so aufgeschrieben sein, dass ihn ein verständiger Leser gut nachvollziehen kann."
