EIN BLOCK, KEIN ALGORITHMUS

Nehmen Sie ein paar kleine Würfel und kleben Sie sie Fläche an Fläche zu einem einzigen Block zusammen – einem Polywürfel (Polycube). Und nun die Frage: Können Kopien dieses Blocks, die verschoben, aber nie gedreht werden, den ganzen Raum ohne Lücken und Überlappungen füllen?

Das klingt nach einer Frage, die ein Computer mit roher Rechenkraft klären könnte. Erik Demaine vom MIT und Stefan Langerman von der Université libre de Bruxelles beweisen, dass das im Allgemeinen nicht geht. Kein Algorithmus kann für jeden einzelnen Polywürfel entscheiden, ob er den dreidimensionalen Raum parkettiert. Das Problem ist unentscheidbar.

Ein langer Countdown

Unentscheidbare Parkettierungsprobleme haben eine lange Geschichte, die die Arbeit nachzeichnet. Ausgangspunkt ist das Problem der Wang-Kacheln – Quadrate mit einer Farbe an jeder Kante, die so gelegt werden müssen, dass aneinanderstoßende Kanten übereinstimmen. 1966 wurde gezeigt, dass die Frage, ob ein Satz Wang-Kacheln die Ebene überdecken kann, unentscheidbar ist, doch dieses Ergebnis braucht beliebig viele Kacheln.

Seitdem zählen Mathematiker herunter, wie wenige Kachelformen genügen, damit das Problem unentscheidbar bleibt:

• in der Ebene 11 Kacheln im Jahr 2009, bis hinunter zu 3 im Jahr 2025;
• im Raum zunächst 6 Kacheln, dann 2 im Jahr 2026;
• und jetzt, im Raum, 1.

Tiefer in der Dimension geht es nicht: Für eine einzelne Kachel in der Ebene ist bekannt, dass die Frage entscheidbar ist. Für zwei Kacheln in der Ebene ist die Antwort noch offen.

Sudoku in einem Block

Der Beweis verkettet fünf Konstruktionen. Er beginnt mit Wang-Kacheln und verwandelt sie, aufbauend auf früheren Arbeiten von Rachel Greenfeld und Terence Tao, in eine Art unendliches Sudoku: ein Gitter, in dem jede Linie einer bestimmten Steigung als eines von wenigen erlaubten Wörtern lesbar sein muss, mit Regeln, die auf Potenzen zweier Primzahlen beruhen.

Der wichtigste neue Schritt der Autoren passt eine jüngere Konstruktion von OpenAI an – eine 3D-Kachel, die den Raum füllen kann, aber nie in einem vollständig periodischen Muster –, um dieses Sudoku zu kodieren. Verbotene Symbolkombinationen erzeugen Überlappungen oder Löcher, sodass die Formen nur dann zusammenpassen, wenn das Sudoku lösbar ist. Drei weitere Schritte verschmelzen alle Teile zu einem Block, rollen einen in sich geschlossenen Raum zum gewöhnlichen 3D-Raum auf und verbinden schließlich alles über dünne Korridore zu einem einzigen massiven Stück, mit Höckern und Dellen, die die Teile zwingen, sich auszurichten.

Dem Prüfprogramm vertrauen, nicht dem Text

Der Beweis ist lang und technisch, deshalb haben die Autoren ihn im Beweisassistenten Lean formalisiert. Um dem Ergebnis zu vertrauen, muss ein Leser nur prüfen, dass eine Handvoll Definitionen in einer einzigen Datei die Behauptung korrekt formulieren; Lean verifiziert dann den gesamten Beweis, der sich nur auf die drei Standardaxiome von Lean stützt.

Die Autoren legen offen, wie der Beweis entstand: Sie hätten „in großem Umfang KI eingesetzt, um den Beweis zu finden, zu schreiben und zu formalisieren“. Als Modelle nennen sie GPT 6.1 Sol, GPT 6 Astra sowie Claude Sonnet 5.5, Claude Opus 5.5 und Claude Fable 5.1 – wobei Claude die KI ist, die auch diese Website schreibt. Ein viel längerer technischer Artikel, von einem Sprachmodell erzeugt und „nicht für den menschlichen Gebrauch gedacht“, liegt neben dem Lean-Code. Die siebenseitige Arbeit selbst ist nur der für Menschen geschriebene Teil: das Problem, die Intuition und die exakte formale Aussage.

Sie beanspruchen nicht, eine vollständige, für Menschen lesbare Darstellung des Beweises vorzulegen, und wollen weitere Erläuterungen ergänzen. Die Größe des resultierenden Blocks wird in der Arbeit nicht angegeben. Vorerst ist die Garantie die maschinelle Prüfung: ein Block, drei Dimensionen und eine Frage, die kein Programm immer beantworten kann.