Magisches Sechseck: mit KI für alle Größen gefunden

Kategorien: Künstliche Intelligenz

Das Wabenrätsel hat jetzt eine Antwort für jede Größe. Den Beweis fand der Autor mit Hilfe von KI und wurde vom Beweisprogramm Lean maschinell geprüft, eine unabhängige Begutachtung steht noch aus. Hier wird er ohne Fachsprache erklärt.

Ein magisches Sechseck ist ein mathematisches Zahlenrätsel, das mit Wabenfeldern gespielt wird. Der Beweis, dass es solche Sechsecke in jeder Größe gibt, wurde mithilfe von KI gefunden und von Lean maschinell geprüft. Die automatisierte Beweisführung kostete einige Stunden Rechenzeit.

Der Beitrag erklärt zuerst, was das Rätsel verlangt, und zeichnet den Werdegang vom ersten Sechseck bis zum Beweis nach. Danach folgt die Beweisidee in fünf Bausteinen, jeweils mit einem Bild. Am Ende geht es um die Frage, warum einem computergeprüften Beweis zu trauen ist und was trotzdem ein Mensch kontrollieren muss (hält sich aber in engen Grenzen!).

Magisches Sechseck: Was das Zahlenrätsel fordert

Die Spielfläche ist eine Wabenfigur in Form eines regelmäßigen Sechsecks. Die Größe heißt Ordnung n und gibt an, wie viele Waben auf einer Seite liegen. Ein Sechseck der Ordnung n besteht aus 3n(n−1)+1 Waben. Bei n = 3 sind das 19 Waben, bei n = 10 schon 271.

In die Waben werden ganze Zahlen geschrieben, und zwar so, dass jede gerade Reihe dieselbe Summe ergibt. Gezählt werden die Reihen in allen drei Richtungen der Wabenfigur. In jeder Richtung gibt es 2n−1 Reihen. Die kürzesten am Rand haben n Waben, die mittlere hat 2n−1 Waben.

Das berühmteste magische Hexagon trägt die Zahlen von 1 bis 19 und hat die Ordnung 3. Jede Reihe ergibt 38. Es ist das klassische Sechseck, und es gibt für die Zahlen ab 1 nur diese eine Größe, in der das Rätsel aufgeht. Eine einfache Überlegung zur Teilbarkeit zeigt, dass die nötige Reihensumme nur bei n = 1 und n = 3 eine ganze Zahl wird. Für alle anderen Ordnungen scheitert die klassische Variante also schon im Ansatz.

Deshalb dreht sich die neue Arbeit um eine verwandte Variante. Statt bei 1 zu beginnen, werden die ganzen Zahlen von −K bis K verwendet, jede genau einmal. Dabei ist K = 3n(n−1)/2. Bei n = 3 sind das die Zahlen −9 bis 9, bei n = 10 die Zahlen −135 bis 135. Jede Reihe ergibt 0, und in der Mitte steht die 0.

Das Rätsel klingt harmlos, ist aber schwer. Die Zahl der möglichen Füllungen wächst mit n so schnell, dass Durchprobieren am Rechner nicht weit führt. Gesucht war deshalb ein Bauplan, der für jede Größe funktioniert, und ein Beweis, dass dieser Bauplan wirklich immer aufgeht.

Vom Rätsel von 1887 zum größten bekannten Hexagon: der Werdegang

Das Ursprungsproblem stammt von Ernst von Haselberg und wird meist auf das Jahr 1887 datiert. Einzelne Quellen nennen 1888, die Primärquelle wurde nicht eingesehen. Später fand Adams das klassische Sechseck nach eigener Schilderung im Jahr 1957 erneut und machte es über die Kolumne von Martin Gardner bekannt. Dass diese Lösung bis auf Drehung und Spiegelung die einzige ist, bewies Charles W. Trigg, veröffentlicht 1964. Eine Sammlung dazu führt die Universität Bielefeld, einen Überblick bietet Wolfram MathWorld.

Die Variante mit aufeinanderfolgenden ganzen Zahlen und Summe 0 kam später in den Blick. Zwischen 2004 und 2006 wurden die Ordnungen 4 bis 8 gefunden, die Ordnung 6 im Oktober 2004, die Ordnungen 7 und 8 im Jahr 2006. Bis 2006 war als größte Lösung nur Ordnung 8 bekannt. Kleinere Ordnungen waren da bereits gelöst. Einen Überblick mit Fundstellen liefert die deutsche Wikipedia.

Im Jahr 2024 fand Dr. DSGVO, der Autor dieses Blogs, mit KI eine Lösung der Ordnung 9. Das war damals die größte bekannte Lösung.

Am 2. August 2026 veröffentlichte dann Konstantin Gukov auf seiner Seite New magic hexagons ein Muster. Er suchte Lösungen bis zur Ordnung 21 und erkannte, dass sich daraus wahrscheinlich eine Konstruktionsvorschrift für beliebig große Sechsecke ableiten lässt. Gukov beschrieb dazu einen Algorithmus und eine Beweisskizze, die zuletzt ab Ordnung 114 greifen sollte. Er weist selbst darauf hin, dass diese Skizze nicht in Lean formalisiert und nicht unabhängig geprüft ist. Der Beweis stand damit noch aus.

Für diese Lücke liegt nun ein Beweis für alle Ordnungen ab 3 vor. Er entstand mit KI und ist als Beschreibung vom 21. Oktober 2026 dokumentiert. Von Lean ist er maschinell geprüft, eine unabhängige Begutachtung steht noch aus, und die Lean-Dateien sind noch nicht öffentlich verlinkt. Dazu später mehr.

Magische Sechsecke für alle Größen: Was bewiesen ist

Bewiesen ist: Für jede Ordnung n ab 3 gibt es ein magisches Sechseck mit den Zahlen von −K bis K, in dem jede Reihe in allen drei Richtungen die Summe 0 hat. Auch die verschärfte Fassung ist bewiesen, bei der zusätzlich die 0 in der Mitte steht. Es gibt dabei keine obere Grenze. Gukovs Skizze greift erst ab Ordnung 114, die Ordnungen davor blieben ohne den letzten Baustein offen.

Die Abdeckung ist gestaffelt. Ordnung 2 ist unmöglich, weil sich die sieben Zahlen −3 bis 3 nicht passend verteilen lassen. Dieser Teil gehört nicht zum Lean-Beweis. Für die Ordnungen 3 bis 6 liegen fertige Sechsecke vor, die Lean Zahl für Zahl nachgeprüft hat. Für die Ordnungen 7 bis 61 greift ein allgemeiner Bauplan, ergänzt um je eine geprüfte Lösung eines Teilrätsels. Für die Ordnungen 62 bis 118 gilt dasselbe, nur wurden die nötigen Listen neu berechnet und geprüft. Ab Ordnung 119 genügt ein fester Bauplan, der für jedes n allgemein bewiesen ist.

Zwei Hauptsätze fassen das zusammen. Der erste besagt, dass es für jedes n ab 3 ein magisches Hexagon der Ordnung n gibt. Der zweite sagt dasselbe für die verschärfte Fassung mit der 0 in der Mitte. Beide Sätze haben keine Voraussetzung außer n ≥ 3.

Der Beweis in fünf Bausteinen: Übersicht

Der Beweis lässt sich als Leiter vorstellen. Jeder Baustein verkleinert die Aufgabe, bis am Ende nur noch eine Sitzordnung auf einer Bank übrig bleibt. Die Bausteine 1 bis 4 lagen bereits geprüft vor. Neu ist der fünfte Baustein, die Sitzordnung für jede Größe. Er schließt den Beweis.

Die folgenden Abschnitte gehen die Bausteine der Reihe nach durch. Die ersten drei sind anschaulich, die letzten zwei dürfen etwas technischer sein. Alle Rechnungen wurden mit Lean formal geprüft.

Baustein 1: Ein Sechstel genügt, denn gegenüber steht das Negative

Das ganze Sechseck muss nicht geplant werden, ein Sechstel reicht. Jede Wabe hat eine Gegenwabe, die am Mittelpunkt gespiegelt liegt. Steht in einer Wabe die Zahl a, kommt in die Gegenwabe −a. So ist jede Zahl mit ihrem Negativen verbraucht, und die 0 bleibt für die Mitte.

Das hat eine praktische Folge für die Reihen. Die gespiegelte Reihe hat genau die negative Summe. Ist eine Reihe ausgeglichen, ist es ihr Spiegelbild auch. Reihen durch die Mitte sind sogar von selbst ausgeglichen.

Das Sechseck zerfällt um die Mitte in sechs gleiche Dreiecke. Drei davon sind Gegenwaben-Dreiecke: Ihre Zahlen folgen aus der Spiegelung durch die Mitte mit umgekehrtem Vorzeichen. Zwei weitere sind um 120 Grad gedrehte Kopien des sechsten Dreiecks und bekommen eng verwandte Zahlen. Übrig bleibt ein einziges freies Dreieck mit T = n(n−1)/2 Waben. Bei n = 10 sind das 45 statt 271 Waben.

Die Bedingung „jede Reihe hat Summe 0“ wird dadurch zu einer Bedingung an dieses Dreieck. Je Reihe muss eine gewichtete Summe seiner Einträge null ergeben. Diese Summe heißt im Folgenden Bilanz der Reihe.

Baustein 2: Jede Zahl wird zu Basis plus Ziffer

Im zweiten Schritt wird jede Zahl in zwei Teile zerlegt, in eine Basis und eine Ziffer. Beide Teile werden getrennt ausgeglichen. Weil sich Reihensummen bei einer Addition einfach addieren, ist das Sechseck magisch, sobald beide Teile für sich ausgeglichen sind.

Der Zahlenvorrat 1 bis 3T wird dazu in Dreiergruppen geteilt: k, T+k und 2T+k für k von 1 bis T. Jede Gruppe ist die Basis T+k plus T mal eine Ziffer, wobei die Ziffer −1, 0 oder 1 ist. Beim Sechseck der Ordnung 3 ist T = 3, der Vorrat reicht von 1 bis 9. Die Basis 4 liefert 1, 4 und 7, die Basis 5 liefert 2, 5 und 8, die Basis 6 liefert 3, 6 und 9.

Damit zerfällt die Aufgabe in zwei unabhängige Rätsel. Das erste ist ein Ziffernfeld aus −1, 0 und 1 mit Bilanz null in jeder Reihe. Das zweite ist ein Basisfeld, bei dem die Beträge T+1 bis 2T so verteilt und mit Vorzeichen versehen werden, dass die Bilanz jeder Reihe null ist.

Baustein 3: Das Ziffernfeld wächst wie eine Leiter

Das Ziffernfeld ist für jede Ordnung ab n = 5 vollständig gelöst, und zwar durch Induktion in Dreierschritten. Das Prinzip kennt jede Leiter: Wer die erste Sprosse hat und eine Regel für den Schritt zur nächsten, erreicht jede Sprosse.

Zuerst gibt es fertige, ausgeglichene Ziffernfelder für die Radien 4, 5 und 6. Der Radius ist dabei n−1. Dann gilt eine Anbauregel: Ein ausgeglichenes Ziffernfeld lässt sich um drei neue Schichten am Rand erweitern. Die neuen Schichten sind so gemustert, dass sie sich in jeder Reihe gegenseitig aufheben. Von 4 geht es so zu 7, 10, 13 und weiter, von 5 zu 8, 11 und weiter, von 6 zu 9, 12 und weiter. Damit ist jeder Radius ab 4 erreicht.

Dieser Teil kostet beim Prüfen kaum Rechenzeit. Er löst allerdings nur das erste der beiden Teilrätsel, das Basisfeld bleibt offen.

Baustein 4: Wunschabstände, die sich gegenseitig ausgleichen

Das Basisfeld wird nicht direkt gesucht. Stattdessen wird zuerst für jedes Wabenpaar festgelegt, um wie viel sich seine zwei Basen unterscheiden sollen. Diese Wunschabstände sind für alle Ordnungen ab n = 13 allgemein bewiesen.

Fast alle Waben des Dreiecks bilden Paare, die an seiner Mittelachse gespiegelt liegen. Die eine Wabe eines Paares bekommt ein Minus, die andere ein Plus. In der Bilanz bleibt dann nur der Unterschied der beiden Beträge übrig, der gemeinsame Anteil T fällt weg. Es kommt also nur auf den Abstand der beiden Ränge an. Der Rang ist einfach die Platznummer: Die Basis T+k hat den Rang k.

Die Wunschabstände entstehen in mehreren Schritten. Es gibt Assoziativitätskreise: kleine Muster aus vier Wabenpaaren mit Gewichten +1 und −1 und Bilanz null in jeder Reihe. Der Name stammt von der Rechenregel, dass sich bei Summen die Klammern umsetzen lassen, ohne das Ergebnis zu ändern. Jede Summe solcher Muster hat ebenfalls Bilanz null. Aus vielen Mustern entsteht ein Masterfeld, in dem kein Wabenpaar den Abstand 0 bekommt. Ein Abstand 0 wäre unbrauchbar, weil zwei Waben nie dieselbe Zahl tragen dürfen.

Die Waben auf der Mittelachse haben keinen Partner. Diese bekommen die kleinsten Ränge 1, 2, 3 und so weiter, und das Masterfeld gleicht genau deren Beitrag aus. Die Diagonalwaben tragen zusätzlich den Anteil T, der sich nicht weghebt. Ihn gleichen zwei verzweigte Ketten von Wabenpaaren aus, die Wälder. Deren Abstände werden um etwa T/2 vergrößert, zusammen also um T.

Das Ergebnis ist ein vollständiger Satz von Wunschabständen mit Bilanz null in jeder Reihe, keiner davon null. Die meisten Abstände sind klein und liegen bei höchstens 12. Die Waben der ersten Zeile haben Abstände bis etwa 2n, die Paare der Wälder Abstände nahe T/2.

Baustein 5: Die Sitzordnung für jede Größe

Zuletzt müssen die Ränge 1 bis T tatsächlich verteilt werden, sodass jedes Wabenpaar genau seinen Wunschabstand bekommt. Ab n = 119 geschieht das mit einem festen Bauplan, darunter mit vom Computer gefundenen und von Lean geprüften Listen.

Das lässt sich als Sitzordnung auf einer langen Bank mit T Plätzen vorstellen. Die Diagonalwaben sitzen fest auf den ersten Plätzen 1, 2, 3 und so weiter. Jedes Wabenpaar braucht zwei Plätze im vorgeschriebenen Abstand. Kein Platz darf doppelt besetzt sein. Genau n−1 Plätze bleiben frei. Diese gehen an die Randwaben ohne Partner, und für die ist jeder Platz recht.

Der entscheidende Trick sind Blöcke. Paare mit gleichem Abstand g lassen sich lückenlos stapeln. Bei g = 3 füllen die Paare (1, 4), (2, 5) und (3, 6) die Plätze 1 bis 6 ohne Lücke. Allgemein füllen g Paare mit Abstand g genau 2g aufeinanderfolgende Plätze, dann folgt der nächste Block. So verschwendet jede Abstandsgruppe höchstens g−1 Plätze am Ende ihres letzten Blocks. Die Gruppen mit den Abständen 1 bis 12 kosten zusammen höchstens 0+1+…+11 = 66 Plätze.

Die Bank wird von vorne nach hinten in fünf Zonen aufgeteilt. In der ersten Zone sitzt die Diagonale. Es folgt das Sternfenster, in dem eine besondere Reihe von Paaren wie Regenbögen ineinander geschachtelt wird und in die Lücken Paare mit den Abständen 6 und 8 passen. Im Waldfenster (von "Forrest") sitzen Paare mit sehr großen Abständen, ihre Partner landen weit hinten in einem reservierten Bereich. Danach kommen die Restklassen, also alle übrigen Paare mit den Abständen 1 bis 12 in Blöcken. Zuletzt nehmen die n−1 Randwaben die Plätze, die übrig bleiben.

Warum greift der Bauplan erst ab n = 119? Die Bank ist fast auf den Platz genau voll. Frei bleiben dürfen nur so viele Plätze, wie es Randwaben ohne Partner gibt, nämlich n−1. Der Bauplan verliert höchstens 117 Plätze: 18 im Sternfenster, 66 in den Blöcken, 21 im Waldfenster und 12 beim Überspringen. Er geht also auf, sobald n−1 mindestens 118 ist. Bei n = 119 sind 118 Plätze frei und höchstens 117 gehen verloren, es bleibt also ein Platz Reserve.

Für die kleineren Größen hat ein Computerprogramm passende Sitzordnungen gesucht und als Zahlenliste gespeichert. Diese Listen heißen Zertifikate. Lean prüft jedes Zertifikat selbst nach, statt dem Suchprogramm zu vertrauen.

Warum dem Beweis zu trauen ist: Lean prüft jeden Schritt

Der Beweis ist nicht nur aufgeschrieben, sondern Zeile für Zeile von einem Beweisprüfer kontrolliert. Lean ist eine Programmiersprache für mathematische Beweise. Jeder Schluss wird so genau definiert, dass der Computer ihn nachrechnen kann. Lücken oder ein „offensichtlich“ gibt es dort nicht. Ein Fehler würde die Übersetzung abbrechen lassen.

Genutzt wird dabei Mathlib, die große gemeinsame Bibliothek bereits geprüfter Mathematik für Lean, etwa für Rechenregeln mit endlichen Mengen und Summen. Im fertigen Beweis kommt kein einziges „sorry“ vor ("sorry" wäre ein Beleg für einen falschen Beweis). Es gibt auch kein eigenes Axiom (eine unbewiesene Grundannahme) und kein Vertrauen in übersetzten Programmcode. Lean kann am Ende auflisten, auf welchen Grundannahmen ein Satz ruht. Hier sind es nur die drei üblichen, auf denen praktisch die gesamte Mathlib aufbaut: propext, Classical.choice und Quot.sound.

Die Python-Programme, die Zertifikate und Bauplan gefunden haben, müssen nicht fehlerfrei sein. Ein falsches Zertifikat oder ein falscher Bauplan würde von Lean abgelehnt. Das ist der eigentliche Gewinn beim Einsatz von KI und Suchprogrammen: Die Werkzeuge dürfen raten, die Prüfung ist trotzdem streng.

Was ein Mensch prüfen muss: die Definition in fünf Zeilen

Eine Grenze gilt für jeden computergeprüften Beweis: Die Definition am Anfang wird nicht geprüft, sondern vorausgesetzt. Im vorliegenden Fall ist die Definition nur fünf Zeilen lang, und sie sagt in Alltagssprache dies: Es gibt eine Füllung der Waben mit ganzen Zahlen. Keine zwei Waben tragen denselben Wert. Die verwendeten Werte sind genau die Zahlen von −K bis K. Jede Reihe in jeder der drei Richtungen hat die Summe 0. In der verschärften Fassung steht außerdem die 0 in der Mitte.

Drei mögliche Schlupflöcher sind ausgeschlossen. Erstens passen Zellen und Zahlen zusammen: Das Sechseck hat 3n(n−1)+1 Waben, und von −K bis K gibt es genau so viele Zahlen, „jede Zahl genau einmal“ ist also erzwungen. Zweitens zählen Werte außerhalb der Wabe nicht, alle Bedingungen beziehen sich nur auf Zellen im Sechseck. Drittens sind Reihen außerhalb der Wabe leer, ihre Summe ist automatisch 0, was harmlos ist. Die Formel für K benutzt ganzzahlige Division, das ist unbedenklich, weil n(n−1) immer gerade ist.

Bei der Prüfung fiel außerdem eine Lücke auf, die inzwischen geschlossen ist. Die ursprüngliche Definition verlangte die 0 in der Mitte nicht ausdrücklich. Die Konstruktion liefert sie zwar immer, weil gespiegelte Waben entgegengesetzte Werte tragen. Trotzdem gibt es jetzt die verschärfte Definition mit der Zusatzbedingung, dass die Mitte 0 ist, und der zweite Hauptsatz beweist sie für alle n ab 3.

Ein Restmisstrauen bleibt, wie bei jedem formalen Beweis. Es betrifft den kleinen Prüfkern von Lean und die Grunddefinitionen von Mathlib, etwa für Summen und Intervalle. Verwendet wurde eine Vorabversion von Lean 4. Außerdem lief die Prüfung bisher in einer einzigen Umgebung. Sicherer wird es, wenn jemand die Dateien unabhängig auf einem eigenen Rechner übersetzt. Optional kann ein separates Kontrollprogramm wie lean4checker die fertigen Beweisdateien noch einmal nachprüfen. Für kleine Größen lässt sich zudem ein konkretes Sechseck ausgeben und von Hand nachrechnen. Das beweist nichts zusätzlich, zeigt aber anschaulich, dass die Definition das Gemeinte trifft.

Zahlen und Fakten zum Beweis

Zur Aussage: Bewiesen ist ein magisches Hexagon mit Summe null für jede Ordnung n ab 3, auch mit der 0 in der Mitte. Fertige Hexagone gibt es für n = 3 bis 6. Für n = 7 bis 118 liefern Zertifikate die Lösung des Basisrätsels, davon sind 57 neu, nämlich die für n = 62 bis 118. Der allgemeine Bauplan gilt ab n = 119, das entspricht dem Radius 118. Er verliert höchstens 117 Plätze und lässt bei n = 119 mindestens einen Platz Reserve. Die größte Zertifikat-Ordnung ist n = 118, das entspricht 6 903 Waben im Dreieck.

Zum Umfang: Die Bausteine 1 bis 4 und die Zertifikate bis n = 61 sind in einer Datei zusammengeführt, die 2 713 Zeilen umfasst. Baustein 5 besteht aus 40 Dateien mit rund 7 000 Zeilen. Der größte Speicherbedarf liegt bei 5,9 Gigabyte, und zwar bei einer Datei zur ersten Zeile des Bauplans. Verwendet wurden Lean 4 und Mathlib. Nur 3 Axiome wurden verwendet, offene Lücken gibt es keine.

Zur Rechenzeit: Der Neubau von Baustein 5 dauert etwa 38 Minuten, die Zertifikate benötigen parallel etwa 23 Minuten. Einzelne Dateien brauchen deutlich länger. Die Datei mit den Bausteinen 1 bis 4 benötigt 460 Sekunden, die Hilfsdatei mit den Formeln der Wunschabstände 897 Sekunden, die Zertifikate für n = 62 bis 89 weitere 437 Sekunden und die für n = 90 bis 117 weitere 927 Sekunden. Die Dateien zur ersten Zeile brauchen zusammen etwa 18 Minuten. Diese Zeiten beschreiben den Neubau der fertigen Prüfung. Die gesamte automatisierte Beweisführung mit Suche und Entwicklung kostete einige Stunden.

Zu den Vortests: Der Bauplan wurde vor dem Lean-Beweis numerisch getestet, als exakte Nachbildung der Definitionen für die Radien 118 bis 450. Die Hilfsaussagen wurden bis zum Radius 20 000 geprüft. Diese Tests waren nur eine Vorprüfung, der Beweis selbst ist der Lean-Text.

Wie es weitergeht: offene Fragen und Einordnung

Gukovs Arbeit und der Lean-Beweis ergänzen sich. Gukov lieferte das Muster, die Konstruktion und eine Skizze mit der Grenze 114. Die Skizze rechnete die Lücken der ersten Zeile und der Wälder nicht nach. Naiv gesetzt, hätten dort zusammen etwa 2n bis 3n Plätze gefehlt, mehr als die erlaubten n−1. Der Lean-Beweis setzt an genau dieser Stelle an. Er liefert Formeln für die Wunschabstände, einen Packungsplan mit höchstens 117 verlorenen Plätzen statt 2n bis 3n und neue Zertifikate für die Ordnungen 62 bis 118. Damit sind alle Ordnungen ab 3 abgedeckt.

Offen bleibt zunächst die unabhängige Kontrolle: ein Nachbau auf einem fremden Rechner (wurde bereits vom Autor erbracht) und eine Begutachtung durch Fachleute. Die Lean-Dateien werden demnächst öffentlich bereitgestellt. Außerdem stellt Gukov auf seiner Seite eine Frage, die der Beweis nicht beantwortet: Warum wirken die Zellwerte wie zufällig, während die zugehörigen Potentialfelder glatt aussehen? Weitere Varianten des Rätsels sind denkbar, versprochen wird dazu nichts.

Ein Rätsel, das bei einer Wabenfigur mit 19 Feldern begann, ist für jede Größe gelöst. Dazu brauchte es zuerst die Idee eines Menschen, dann KI als Sucher und Beweis-Assistent und zuletzt einen Prüfer, der keinem der Beteiligten glaubt, sondern jeden Schritt nachrechnet.