Zahlen, bitte! Mit 800 CPU-Kernen zur Zahl 7825

Zahlen, bitte!

In dieser Rubrik stellen wir immer dienstags verblüffende, beeindruckende, informative und witzige Zahlen aus den Bereichen IT, Wissenschaft, Kunst, Wirtschaft, Politik und natürlich der Mathematik vor.

• Alle Artikel zu "Zahlen, bitte!"

Den Satz des Pythagoras und die Gleichung a² + b² = c² dürften so ziemlich alle aus ihrem Matheunterricht kennen. Manche erinnern sich vielleicht auch an die Zwölfknotenschnur, mit der man einen rechten Winkel darstellen kann, indem man ein Dreieck mit Kantenlängen 3:4:5 legt. Das klappt, weil die Zahlen eben den Satz des Pythagoras 3² + 4² = 9 + 16 = 25 = 5² erfüllen. Solche ganzzahlige Lösungen der Gleichung nennt man "pythagoräische Zahlentripel". Andere kleine pythagoräische Zahlentripel sind beispielsweise 5² + 12² = 13² oder 6² + 8² = 10². Und wo ist jetzt das Problem?

Zahlenrätsel

Mathematiker haben bekanntermaßen einen angeborenen Spaß an Zahlenrätseln und Fragen, die sich sonst keiner stellt. Auftritt des bekannten US-Mathemagikers Ronald Graham: Er lobte in den achtziger Jahren ein symbolisches Preisgeld in Höhe von 100 US-Dollar für diejenigen aus, die das aus der Ramsey-Theorie stammende kombinatorische Problem boolescher pythagoräischer Zahlentripel lösen. Die Fragestellung lautet: Kann man die Zahlen von 1 bis n so in zwei Gruppen (rot oder blau eingefärbt) aufteilen, dass keine von beiden ein pythagoräisches Tripel enthält? Sprich, es dürfen nicht alle drei Zahlen eines solchen Tripels dieselbe Farbe haben.

Für kleine n kann man das noch durchprobieren. Allerdings wird es schnell unübersichtlich, weil es 2ⁿ Möglichkeiten gibt; schon bei n = 100 wären es schon mehr als 10³⁰ Möglichkeiten. Also haben die drei Forscher Marijn J. H. Heule, Oliver Kullmann und Victor W. Marek die 800 CPU-Kerne des Stampede Supercomputers (Texas Advanced Computing Center) auf das Problem angesetzt. Dabei kam heraus, dass die Färbung bis n = 7824 klappt, danach aber nicht mehr.

Hätten sie nur blind alle Möglichkeiten durchprobieren lassen, müsste man noch lange auf das Ergebnis warten, denn auch ein Supercomputer würde sich an dem Problem die Zähne ausbeißen, wenn man sich nicht geschickt anstellt; immerhin wären 2⁷⁸²⁵ = 3,63 × 10²³⁵⁵ Möglichkeiten zu prüfen.

Maschinengestützter Beweis

Darum haben sie ihre selbst entwickelte "Cube & Conquer"-Methode angewandt, die sich besonders gut für große kombinatorische Probleme eignet. Dazu haben die Forscher zunächst die Fragestellung in ein Erfüllbarkeitsproblem (SAT, englisch "Satisfiability") kodiert, dieses zwecks effizienter Verarbeitung transformiert, aufgeteilt und schließlich dessen Unerfüllbarkeit ab n = 7285 bewiesen.

So konnte die Rechenzeit des Supercomputers auf nur zwei Tage gedrückt werden. Der Beweis hat im DRAT-Format (Deletion Resolution Asymmetric Tautology) eine Gesamtgröße von 200 Terabyte und wird darum als bisher "größter" mathematischer Beweis aller Zeiten gefeiert.

Die Wissenschaftler haben alle einzelnen Beweisschritte durch Software – Theorembeweiser und Beweis-Checker – auf Richtigkeit geprüft. Der Datensatz (komprimiert 68 GByte) steht zur Kontrolle durch Dritte zur Verfügung. Interessierte finden die vom Autoren hier verschwiegenen (und sein Verständnis übersteigenden) Details in der Veröffentlichung "Solving and Verifying the boolean PythagoreanTriples problem via Cube-and-Conquer" (PDF).

So richtig befriedigend ist der maschinengestützte Beweis aber nicht. Den meisten Mathematikern ist eine klassische Beweisführung lieber, bei der dann hoffentlich auch klar werden würde, warum das Einfärben ausgerechnet ab n = 7825 nicht mehr funktioniert. Möglicherweise liefert das Resultat aber Denkanstöße für einen Beweis ohne Computer-Unterstützung.

Für Ron Graham haben Heule, Kullmann und Marek die Herausforderung aber erfüllt. Er hat ihnen kürzlich die 100 US-Dollar als symbolischen Preis überreicht, was laut den Wissenschaftlern nicht einmal die Stromrechnung für den Beweis decken würde ... (vza)