Puristen lehnen die Verwendung von Computern für mathematische Beweise nach wie vor ab. Der österreichische Mathematiker Bruno Buchberger, Gründer des Instituts für Symbolisches Rechnen der Linzer Johannes-Kepler-Universität und des Softwareparks Hagenberg, sucht allerdings längst nach Möglichkeiten, den Beweisprozess zu automatisieren. Er ist international bekannt durch einen Algorithmus, mit welchem bestimmte fundamentale Probleme in der abstrakten Mathematik, die bis dahin als nicht mit Computern behandelbar galten, gelöst werden können. Und zwar durch die Rückführung der Probleme auf das Berechnen so genannter "Gröbner-Basen". Der Algorithmus ist heute in allen kommerziellen mathematischen Softwaresystemen wie beispielsweise Mathematica eingebaut und macht die Lösung einer Vielzahl auch praktischer Probleme möglich - zum Beispiel in der Robotik und in der Kryptografie.Mit seiner neuen Lazy-Thinking-Methode geht Buchberger nun einen Schritt weiter: Das Verfahren spürt solche Lösungsalgorithmen systematisch auf. "Man muss nur mehr das Problem hinschreiben, und der Algorithmus kommt - in vielen Fällen - automatisch heraus", macht Buchberger klar, was "lazy" in diesem Zusammenhang bedeutet. Das Verfahren liefert dabei nicht nur den Lösungsalgorithmus, sondern zugleich den Beweis, dass er korrekt ist - indem es für jede zulässige Eingabe die richtige Lösung ausspuckt. Wie ein Taschenrechner, der immer richtig multipliziert, gleichgültig, welche Zahlen man eintippt. Lazy Thinking ist im Softwaresystem Theorema implementiert, an dessen Entwicklung Buchberger und seine Mitarbeiter seit etwa zehn Jahren arbeiten. Ziel ist, Mathematikern ein Werkzeug zur Verfügung zu stellen, das sie durch den gesamten mathematischen Erfindungs- und Verifikationsprozess begleitet: von der Spezifikation eines Problems bis zur Entwicklung eines Lösungsalgorithmus für das Problem und seine Anwendung am Computer. Dass dabei Verfahren wie Lazy Thinking Mathematikern auch jahrelange Arbeit ersparen können, zeigte Buchberger im Selbstexperiment. Er hat das Verfahren auf das Problem der Berechnung von Gröbner-Basen angewandt, für dessen Erfindung er seinerzeit zwei Jahre gebraucht hat, nachdem schon vorher viele andere wie Buchbergers Lehrer Wolfgang Gröbner an dem Problem seit Jahrzehnten gearbeitet hatten. Der Vergleich machte sicher: Die Lazy-Thinking-Methode lieferte den Algorithmus samt Korrektheitsbeweis auf einem Laptop in wenigen Minuten. (gröm, Der Standard, Printausgabe, 13.12.2004)