Hagenberg/Wien - Wie ist Pythagoras draufgekommen? Einen mathematischen Satz wie jenen, der besagt, dass a² + b² = c² bei allen rechtwinkeligen Dreiecken richtig ist, erstmals zu formulieren gilt als Sternstunde in der Geschichte der Mathematik. Das Finden eines Beweises, der ein für alle Mal belegt, dass diese Einsicht in allen möglichen Fällen - nicht nur in jenen, die man in Beispielen beobachtet - stimmt, ist eine der grundlegenden Aufgaben der Theoretiker. "Wer das erste Mal einen Beweis für eine nicht triviale Aussage findet, zählt deshalb auch zu den Denkhelden der Geschichte."

Bruno Buchberger, Mathematiker und Gründer sowohl des Research Institute for Symbolic Computation (Risc) der Johannes-Kepler-Universität (JKU) als auch des Softwareparks Hagenberg, geht im Standard-Gespräch bis zu Pythagoras zurück, um die Grundlagen seines Theorema-Projekts zu erklären. Die Aufgabe, die es sich stellt, ist auch von entsprechend universeller Natur: Es will die Generierung mathematischer Erkenntnisse und das Finden entsprechender Beweise mithilfe von Computern automatisieren.

Der Satz des Pythagoras ist - zumindest aus der Sicht zweieinhalbtausend Jahre nach seiner Entdeckung - eine der einfachsten Einsichten und kann in wenigen Denkschritten nachvollzogen werden. Gegenwärtige Probleme und mathematische Vermutungen sind ungleich komplexer und harren oft Jahrzehnte lang eines Beweises.

Die Anwendung bereits gefundener mathematischer Einsichten hat man längst den Computern anvertraut. Sie errechnen damit Flugbahnen zu anderen Planeten oder komplexe thermodynamische Prozesse.

Mehr und mehr Mathematiker befassen sich heute damit, den Computer nun "in den ersten Stock der Mathematik" zu holen, um ihn dort eigenständig Argumentationsketten finden zu lassen und um sich selbst mit anderen Problemen zu beschäftigen, die noch nicht automatisierbar sind.

"Weltweit befassen sich etwa 30 oder 40 Gruppen mit diesem Themengebiet des ,automated reasoning'", erklärt Buchberger. Er selbst begann 1995, sich dem damals neuen Gebiet zu widmen. Die Software, die er gemeinsam mit Wolfgang Windsteiger und weiteren Mitgliedern seiner Theorema-Gruppe entwickelte, unterstützt bereits den komplexen Erfindungs- und Beweisvorgang in bestimmten Bereichen der Mathematik.

Methoden der Beweissuche

Die Methodik, auf der die Algorithmen der Theorema-Software aufbauen, ist in zwei Zugänge aufgeteilt: Mittels einer Top-down-Methode wird im Rahmen der Prädikatenlogik versucht, einen Satz so zu beweisen, "als ob man das gesamte Wissen, das man dazu bräuchte, schon hat", erläutert Buchberger. "Wenn ich alle Hilfssätze bereits hätte, wie könnte ich den Beweis vollenden", lautet die Frage dahinter.

Ein schwieriger Satz zerfällt auf diese Art in eine Kaskade einfacherer Teile, die selbst erst bewiesen werden müssen. Kommt man in den Beweisen zu keinem Ende, kann man aus den fehlgeschlagenen Versuchen wiederum hilfreiches Wissen generieren. "Aus der Analyse von ,failing proofs' kommt man so zu möglichen neuen Hilfssätzen", sagt Buchberger.

Die zweite wesentliche Methode verläuft in die entgegengesetzte Richtung: "Die Mathematik besteht aus tausenden Begriffen, Theoremen und Methoden, aber nur aus wenigen Grundprinzipien, wie diese mathematischen Ideen aus einfacheren Begriffen, Theoremen und Methoden aufgebaut sind", sagt der Mathematiker. Diese strukturellen Eigenschaften, die sich immer wieder finden, versucht man zu identifizieren, um daraus "bottom-up" automatisch mathematische Theorien zu entwickeln.

Die Software könnte in Zukunft zum Beispiel auch dazu dienen, auf individuelle Lösungsversuche von Schülern bei ihren mathematischen Aufgaben einzugehen. "Ein kluger Lehrer erkennt die Denkschritte eines Schülers und gibt ihm einen Ratschlag, der für seine konkrete Situation maßgeschneidert ist", sagt Buchberger. "Dieses intelligente mathematische Denken wollen wir mit Theorema unterstützen."

Lösung in wenigen Minuten

Welchen Fortschritt die automatischen Beweise bringen, kann der 71-jährige Buchberger anhand seiner eigenen Biografie veranschaulichen: Im Alter von 23 Jahren legte der Mathematiker mit seiner Theorie der "Gröbner-Basen", die ein sechs Jahrzehnte lang offenes Problem im Bereich nicht-linearer Systeme löste, den Grundstein für seine Professorenkarriere. "Wenn ich das Problem, dessen Lösung damals im Rahmen meiner Dissertation eineinhalb Jahre dauerte, in Theorema eingebe, entsteht der Grundgedanke der Theorie in wenigen Minuten", sagt Buchberger. (Alois Pumhösel, DER STANDARD, 14.5.2014)