Mathematiker stellen sich manchmal für den Laien recht seltsam anmutende Aufgaben. "Planare Partitionen" nennt sich eine davon, bei der es um die Berechnung von Würfeln geht, die nach bestimmten Regeln angeordnet werden müssen. Linzer Forscher haben nun eine 1983 von zwei US-Mathematikern aufgestellte mathematische Vermutung über solche "planare Partitionen" bewiesen. Dies gelang ihnen ausschließlich mit dem Computer, der dafür Monate rechnen musste, und unter Verwendung einer Hilfsformel, die ausgedruckt rund eine Million A4-Seiten umfassen würde. Die Arbeit der Wissenschafter wurde nun in der Fachzeitschrift PNAS veröffentlicht - auf lediglich vier Seiten.
Fixe Regeln
Bei einer "planaren Partition" werden auf einer schachbrettartigen Grundfläche aus würfelförmigen Bauklötzen Türme gebaut, und zwar nach fixen Regeln: Kein Turm darf höher sein als die Länge der Grundfläche und auch nicht höher als ein Turm dahinter oder links davon. Die Mathematiker interessiert nun, wie viele verschiedene Anordnungen sich auf einer bestimmten Grundfläche bauen lassen. Ohne weitere Regeln ist das relativ einfach, schwieriger wird es allerdings, wenn die Anordnung bestimmte Symmetrien aufweisen soll oder andere Vorgaben gemacht werden.
Für eine spezielle Vorgabe, die "total symmetrischen planaren Partitionen", haben schon 1983 George Andrews und David Robbins eine Vermutung für eine allgemeingültige Formel für beliebige Größen vorgelegt. "Das war aber nur eine Vermutung, die fast 30 Jahre unbewiesen geblieben ist", erklärte Manuel Kauers vom Institut für Symbolisches Rechnen der Uni Linz im Gespräch mit der APA. Gemeinsam mit seinem Linzer Kollegen Christoph Koutschan und den US-Mathematiker Doron Zeilberger hat es Kauers in dem vom Wissenschaftsfonds FWF geförderten Projekt nun geschafft, die Vermutung zu beweisen.
"Nur ein paar Monate"
Koutschan hat dabei die zur Berechnung des Beweises notwendigen Programme so optimiert, dass die Rechenzeit in Summe "nur ein paar Monate dauerte. Wenn man das so macht wie im Lehrbuch, dann würde das Hunderte von Jahre dauern", so Kauers.
Aber nicht nur die Rechenzeit ist beeindruckend. Für die Beweisführung war es notwendig, den Computer eine Hilfsgleichung berechnen zu lassen. Während die zu beweisende Gleichung "ganz klein ist, das ist nur eine Zeile", so Kauers, ist die Hilfsgleichung für den Beweis deutlich komplexer: Ausgedruckt würde sie rund eine Million A4-Seiten umfassen.
Mit dem vom Computer berechneten Beweisverfahren konnten die Wissenschafter auch zeigen, dass Programme durchaus mathematische Probleme knacken, an denen Mathematiker scheitern. Zumindest für einen gewissen Typ von Problemen liege die Zukunft der Mathematik sicher im Computer, ist Kauers überzeugt. (APA)