Der Beweis aus dem Automaten

4. Juni 2013, 19:57
posten

Mathematiker versuchen, Gleichungen und Ungleichungen mit elektronischer Hilfe beizukommen

Man könnte annehmen, dass sich Mathematik und Computer ohnehin gut verstehen und dass zu diesem Verhältnis nicht mehr viel beigetragen werden könnte. Wenn es aber richtig kompliziert wird, ist das ganz und gar nicht der Fall. Die Mathematiker müssen dann gehörig nachhelfen, damit sie der Computer einigermaßen versteht und ihnen helfen kann, ihre komplexen Aufgaben zu lösen.

Gleichungen und Ungleichungen kommen in vielen Bereichen der Mathematik vor. Ab einem gewissen Komplexitätsgrad kommt man aber nicht mehr mit systematischen Lösungsansätzen ans Ziel. Wer die ausgetretenen Pfade verlässt, muss selbst einen Weg finden. Bisher standen die Mathematiker dabei mit Kreide vor einer Tafel oder saßen mit dem Bleistift in der Hand über einem Blatt Papier, wären aber nicht auf die Idee gekommen, eine niedrige mathematische Existenz wie einen Computer um substanzielle Hilfe zu bitten.

Mittlerweile hat sich das geändert. In relativ neuen Forschungsgebieten wie der Computeralgebra ringt man den Rechenmaschinen Hilfe bei der symbolischen Lösung schwieriger Gleichungen ab, Gleichungen, die ohne Computer vielleicht überhaupt nicht aufgelöst werden können. Auch am Research Institute for Symbolic Computation (Risc) der Johannes-Kepler- Universität Linz wird das Feld der Mathematik elektronisch beackert. Die Mathematikerin Veronika Pillwein beschäftigt sich etwa in der Gruppe " Algorithmische Kombinatorik" (Leitung: Peter Paule) damit, dem Computer beizubringen, komplexe Ungleichungen zu beweisen.

Die Frage, ob ein Term tatsächlich größer oder gleich null ist, klingt weniger kompliziert, als sie sein kann. "Ungleichungen sind insgesamt schwieriger zu handhaben als Gleichungen, auch für Menschen", sagt Pillwein. Man müsse mehr Techniken einsetzen, es gebe weniger methodische Zugänge, man müsse die richtige Idee für das Problem haben. Und welcher Computer hat schon eine Idee?

Unendliche Folgen

Eine Lösung mag gelingen, indem aus diskreten, endlichen Werten durch Rekursion eine unendliche Folge generiert, eine Funktion durch sich selbst erklärt wird. Dem Computer muss man aber zuerst in einem Algorithmus eine Bildungsvorschrift mitgeben, damit er den Beweis antreten kann. Man benötigt jedenfalls eine endliche Beschreibung, diskrete Parameter mit endlichen Informationen. Der Computer kann nicht ewig rechnen.

Für ihn muss das mathematische Problem richtig strukturiert, zurechtgeschneidert werden. Es muss so aufgebaut werden, dass er überhaupt ein Ergebnis liefern kann und tatsächlich das beweist, was zu zeigen ist, erklärt Pillwein. Und der Algorithmus muss vor allem zu einem Ende kommen, terminieren. Auch hier: "Das Programm muss tun, für was es gedacht ist", so die Mathematikerin.

Ungleichungen tauchen in vielen mathematischen Zusammenhängen auf, etwa in der Konstruktion und der Modellierung konkreter Objekte. Pillwein konnte einen besonderen Erfolg verbuchen, indem sie eine Ungleichung aus dem Bereich der speziellen Funktionen mithilfe des Computers bewies, die von einem numerischen Mathematiker vermutet wurde. Spezielle Funktionen haben grundlegende Bedeutung und spielen eine tragende Rolle in der Mathematik und in ihren Anwendungen, etwa in der Physik. Die numerische Mathematik beschäftigt sich damit, Gleichungen zahlenmäßig zumindest näherungsweise zu lösen.

Partielle Differenzialgleichung

Eine auf anderem Wege nicht lösbare Ungleichung aus dem Gebiet der Fuzzy Logic, jener Theorie, die sich mit der Beschreibung von Unsicherheiten, jenem Bereich zwischen wahr und falsch, beschäftigt, konnte von Pillwein und Kollegen durch einen automatisierten Beweis gelöst werden.

Partielle Differenzialgleichungen, die oft physikalische Prozesse beschreiben, die helfen, Autos zu entwickeln und Brücken zu bauen, und die oft durch die sogenannte Finite-Elemente-Methode gelöst werden können, sind ein weiteres Problem, an dem Pillwein mit ihren Algorithmen arbeitet. Am Anfang stehen vielleicht Messdaten über eine Temperatur an der Oberfläche eines Gegenstandes. Am Ende kommt eine näherungsweise Beschreibung eines dynamischen Vorgangs heraus: eine Wärmeverteilung, Informationen über die Beschaffenheit geologischer Schichten oder ein Teil eines Wettermodells. (Alois Pumhösel, DER STANDARD, 5.6.2013)

Share if you care.