Magisch zeshoek: met AI gevonden voor elke grootte

De honingraatpuzzel heeft nu een antwoord voor elke grootte. De auteur vond het bewijs met behulp van AI en het werd machinaal gecontroleerd door de bewijsassistent Lean; een onafhankelijke beoordeling staat nog open. Hier wordt het zonder vakjargon uitgelegd.

Een magisch zeshoek is een getallenpuzzel die op honingraatcellen wordt gespeeld. Het bewijs dat zulke zeshoeken in elke grootte bestaan, werd met behulp van AI gevonden en door Lean machinaal gecontroleerd. Het geautomatiseerde zoeken naar het bewijs kostte enkele uren rekentijd. Hier wordt uitdrukkelijk de wiskundige puzzel bedoeld en niet de gelijknamige term uit de economische politiek.

Dit artikel legt eerst uit wat de puzzel vraagt en volgt de weg van het eerste zeshoek tot het bewijs. Daarna volgt het bewijsidee in vijf bouwstenen, elk met een afbeelding. Het slot gaat over de vraag waarom een door de computer gecontroleerd bewijs te vertrouwen is, wat een mens toch moet controleren en welke getallen en feiten achter het resultaat staan.

Magisch zeshoek: wat de getallenpuzzel vraagt

Het speelveld is een honingraatfiguur in de vorm van een regelmatige zeshoek. De grootte heet orde n en geeft aan hoeveel cellen er op één zijde liggen. Een zeshoek van orde n bestaat uit 3n(n−1)+1 cellen. Bij n = 3 zijn dat 19 cellen, bij n = 10 al 271.

In de cellen worden gehele getallen geschreven, en wel zo dat elke rechte rij dezelfde som heeft. De rijen worden geteld in alle drie de richtingen van de honingraatfiguur. In elke richting zijn er 2n−1 rijen. De kortste aan de rand hebben n cellen, de middelste heeft 2n−1 cellen.

Het beroemdste magische zeshoek draagt de getallen 1 tot en met 19 en heeft orde 3. Elke rij heeft som 38. Het is het klassieke zeshoek, en voor de getallen vanaf 1 is dit de enige grootte waarin de puzzel opgaat. Een eenvoudige deelbaarheidsredenering laat zien dat de vereiste rijsom alleen bij n = 1 en n = 3 een geheel getal wordt. Voor alle andere ordes mislukt de klassieke variant dus al in de aanzet.

Daarom draait het nieuwe werk om een verwante variant. In plaats van bij 1 te beginnen worden de gehele getallen van −K tot K gebruikt, elk precies één keer. Hierbij is K = 3n(n−1)/2. Bij n = 3 zijn dat de getallen −9 tot 9, bij n = 10 de getallen −135 tot 135. Elke rij heeft som 0 en de 0 staat in het midden.

De puzzel klinkt onschuldig, maar is moeilijk. Het aantal mogelijke invullingen groeit met n zo snel dat uitproberen op de computer niet ver komt. Gezocht werd daarom een bouwplan dat voor elke grootte werkt, en een bewijs dat dit bouwplan echt altijd opgaat.

Van de puzzel uit 1887 tot het grootste bekende zeshoek: de geschiedenis

Het oorspronkelijke probleem komt van Ernst von Haselberg en wordt meestal op het jaar 1887 gedateerd. Enkele bronnen noemen 1888, de primaire bron is niet ingezien. Later vond Adams het klassieke zeshoek naar eigen zeggen in 1957 opnieuw en maakte het bekend via de column van Martin Gardner. Dat deze oplossing op draaiing en spiegeling na de enige is, bewees Charles W. Trigg, gepubliceerd in 1964. Een verzameling hierover wordt bijgehouden door de Universiteit van Bielefeld, een overzicht biedt Wolfram MathWorld.

De variant met opeenvolgende gehele getallen en som 0 kwam later in beeld. Tussen 2004 en 2006 werden de ordes 4 tot en met 8 gevonden, orde 6 in oktober 2004, de ordes 7 en 8 in 2006. Tot 2006 was alleen orde 8 als grootste oplossing bekend. Kleinere ordes waren toen al opgelost. Een overzicht met vindplaatsen biedt de Duitse Wikipedia, waarvan de datumvermeldingen deels onderbouwing missen.

In 2024 vond Dr. DSGVO, de auteur van deze blog, met AI een oplossing van orde 9. Dat was toen de grootste bekende oplossing.

Op 2 augustus 2026 publiceerde Konstantin Gukov vervolgens op zijn pagina New magic hexagons een patroon. Hij zocht oplossingen tot en met orde 21 en herkende dat daaruit waarschijnlijk een constructievoorschrift voor willekeurig grote zeshoeken af te leiden is. Gukov beschreef daarbij een algoritme en een bewijsschets die uiteindelijk vanaf orde 114 zou moeten werken. Hij wijst er zelf op dat deze schets niet in Lean is geformaliseerd en niet onafhankelijk is gecontroleerd. Het bewijs was daarmee nog niet geleverd.

Voor deze leemte ligt er nu een bewijs voor alle ordes vanaf 3. Het ontstond met AI en is gedocumenteerd als beschrijving van 21 oktober 2026. Lean heeft het machinaal gecontroleerd, een onafhankelijke beoordeling staat nog open en de Lean-bestanden zijn nog niet openbaar gelinkt. Daarover later meer.

Magische zeshoeken voor alle groottes: wat is bewezen

Bewezen is: voor elke orde n vanaf 3 bestaat er een magisch zeshoek met de getallen van −K tot K, waarin elke rij in alle drie de richtingen som 0 heeft. Ook de aangescherpte versie is bewezen, waarbij bovendien de 0 in het midden staat. Er is hierbij geen bovengrens. Gukovs schets werkt pas vanaf orde 114, de ordes daarvoor bleven zonder de laatste bouwsteen open.

De dekking is gelaagd. Orde 2 is onmogelijk, omdat de zeven getallen −3 tot 3 zich niet passend laten verdelen. Dit deel hoort niet bij het Lean-bewijs. Voor de ordes 3 tot en met 6 liggen kant-en-klare zeshoeken klaar die Lean getal voor getal heeft nagecontroleerd. Voor de ordes 7 tot en met 61 geldt een algemeen bouwplan, aangevuld met telkens één gecontroleerde oplossing van een deelpuzzel. Voor de ordes 62 tot en met 118 geldt hetzelfde, alleen werden de benodigde lijsten opnieuw berekend en gecontroleerd. Vanaf orde 119 volstaat een vast bouwplan dat voor elke n algemeen is bewezen.

Twee hoofdstellingen vatten dit samen. De eerste zegt dat er voor elke n vanaf 3 een magisch zeshoek van orde n bestaat. De tweede zegt hetzelfde voor de aangescherpte versie met de 0 in het midden. Beide stellingen hebben geen voorwaarde behalve n ≥ 3.

Het bewijs in vijf bouwstenen: overzicht

Het bewijs is voor te stellen als een ladder. Elke bouwsteen maakt de opgave kleiner, tot er aan het eind alleen nog een zitorde op een bank overblijft. De bouwstenen 1 tot en met 4 lagen al gecontroleerd klaar. Nieuw is de vijfde bouwsteen, de zitorde voor elke grootte. Die sluit het bewijs af.

De volgende paragrafen behandelen de bouwstenen een voor een. De eerste drie zijn aanschouwelijk, de laatste twee mogen wat technischer zijn. Alle berekeningen zijn door Lean gecontroleerd, in de tekst volstaan daarom de ideeën.

Bouwsteen 1: een zesde volstaat, want tegenover staat het negatieve

Het hele zeshoek hoeft niet gepland te worden, een zesde is genoeg. Elke cel heeft een tegencel die aan het middelpunt gespiegeld ligt. Staat in een cel het getal a, dan komt in de tegencel −a. Zo is elk getal samen met zijn negatieve opgebruikt en blijft de 0 over voor het midden.

Dit heeft een praktisch gevolg voor de rijen. De gespiegelde rij heeft precies de negatieve som. Is een rij in evenwicht, dan is haar spiegelbeeld dat ook. Rijen door het midden zijn zelfs vanzelf in evenwicht.

Het zeshoek valt rond het midden uiteen in zes gelijke driehoeken. Drie daarvan zijn tegencel-driehoeken: hun getallen volgen uit de spiegeling door het midden met omgekeerd teken. Twee andere zijn kopieën van de zesde driehoek, 120 graden gedraaid, en krijgen nauw verwante getallen. Er blijft één vrije driehoek over met T = n(n−1)/2 cellen. Bij n = 10 zijn dat 45 in plaats van 271 cellen.

De voorwaarde „elke rij heeft som 0" wordt daardoor een voorwaarde aan deze driehoek. Per rij moet een gewogen som van haar waarden nul opleveren. Deze som heet hierna de balans van de rij.

Bouwsteen 2: elk getal wordt basis plus cijfer

In de tweede stap wordt elk getal in twee delen gesplitst, een basis en een cijfer. Beide delen worden apart in evenwicht gebracht. Omdat rijsommen bij optelling gewoon optellen, is het zeshoek magisch zodra beide delen afzonderlijk in evenwicht zijn.

De voorraad 1 tot en met 3T wordt daarvoor in groepen van drie verdeeld: k, T+k en 2T+k voor k van 1 tot en met T. Elke groep is de basis T+k plus T maal een cijfer, waarbij het cijfer −1, 0 of 1 is. Bij het zeshoek van orde 3 is T = 3 en loopt de voorraad van 1 tot 9. Basis 4 levert 1, 4 en 7, basis 5 levert 2, 5 en 8, basis 6 levert 3, 6 en 9.

Daarmee valt de opgave uiteen in twee onafhankelijke puzzels. De eerste is een cijferveld van −1, 0 en 1 met balans nul in elke rij. De tweede is een basisveld, waarbij de bedragen T+1 tot en met 2T zo worden verdeeld en van een teken voorzien dat de balans van elke rij nul is.

Bouwsteen 3: het cijferveld groeit als een ladder

Het cijferveld is voor elke orde vanaf n = 5 volledig opgelost, en wel door inductie in stappen van drie. Het principe kent iedereen van een ladder: wie de eerste sport heeft en een regel voor de stap naar de volgende, bereikt elke sport.

Eerst zijn er kant-en-klare, in evenwicht gebrachte cijfervelden voor de stralen 4, 5 en 6. De straal is hierbij n−1. Dan geldt een aanbouwregel: een in evenwicht gebracht cijferveld laat zich met drie nieuwe lagen aan de rand uitbreiden. De nieuwe lagen zijn zo gepatroneerd dat ze elkaar in elke rij opheffen. Zo gaat het van 4 naar 7, 10, 13 en verder, van 5 naar 8, 11 en verder, van 6 naar 9, 12 en verder. Daarmee is elke straal vanaf 4 bereikt.

Dit deel kost bij het controleren nauwelijks rekentijd. Het lost echter alleen de eerste van de twee deelpuzzels op, het basisveld blijft open.

Bouwsteen 4: gewenste afstanden die elkaar opheffen

Het basisveld wordt niet direct gezocht. In plaats daarvan wordt eerst voor elk celpaar vastgelegd hoeveel zijn twee basissen moeten verschillen. Deze gewenste afstanden zijn voor alle ordes vanaf n = 13 algemeen bewezen.

Bijna alle cellen van de driehoek vormen paren die aan de middenas gespiegeld liggen. De ene cel van een paar krijgt een min, de andere een plus. In de balans blijft dan alleen het verschil tussen de twee bedragen over, het gemeenschappelijke aandeel T valt weg. Het komt er dus alleen op aan wat de afstand tussen de twee rangen is. De rang is simpelweg het plaatsnummer: de basis T+k heeft rang k.

De gewenste afstanden ontstaan in meerdere stappen. Er zijn associativiteitscirkels: kleine patronen van vier celparen met gewichten +1 en −1 en balans nul in elke rij. De naam komt van de rekenregel dat bij sommen de haakjes verzet kunnen worden zonder het resultaat te veranderen. Elke som van zulke patronen heeft eveneens balans nul. Uit veel patronen ontstaat een meesterveld, waarin geen enkel celpaar afstand 0 krijgt. Een afstand 0 zou onbruikbaar zijn, omdat twee cellen nooit hetzelfde getal mogen dragen.

De cellen op de middenas hebben geen partner. Die krijgen de kleinste rangen 1, 2, 3 enzovoort, en het meesterveld compenseert precies hun bijdrage. De diagonaalcellen dragen bovendien het aandeel T, dat niet wegvalt. Dat compenseren twee vertakte ketens van celparen, de bossen. Hun afstanden worden met ongeveer T/2 vergroot, samen dus met T.

Het resultaat is een volledige set gewenste afstanden met balans nul in elke rij, waarvan er geen nul is. De meeste afstanden zijn klein en liggen op hoogstens 12. De cellen van de eerste rij hebben afstanden tot ongeveer 2n, de paren van de bossen afstanden dicht bij T/2.

Bouwsteen 5: de zitorde voor elke grootte

Tot slot moeten de rangen 1 tot en met T echt verdeeld worden, zodat elk celpaar precies zijn gewenste afstand krijgt. Vanaf n = 119 gebeurt dat met een vast bouwplan, daaronder met door de computer gevonden en door Lean gecontroleerde lijsten.

Dit is voor te stellen als een zitorde op een lange bank met T plaatsen. De diagonaalcellen zitten vast op de eerste plaatsen 1, 2, 3 enzovoort. Elk celpaar heeft twee plaatsen nodig op de voorgeschreven afstand. Geen plaats mag dubbel bezet zijn. Precies n−1 plaatsen blijven vrij. Die gaan naar de randcellen zonder partner, voor wie elke plaats goed is.

De beslissende truc zijn blokken. Paren met dezelfde afstand g laten zich zonder gaten stapelen. Bij g = 3 vullen de paren (1, 4), (2, 5) en (3, 6) de plaatsen 1 tot en met 6 zonder gat. In het algemeen vullen g paren met afstand g precies 2g opeenvolgende plaatsen, daarna volgt het volgende blok. Zo verspilt elke afstandsgroep hoogstens g−1 plaatsen aan het eind van haar laatste blok. De groepen met de afstanden 1 tot en met 12 kosten samen hoogstens 0+1+…+11 = 66 plaatsen.

De bank wordt van voor naar achter in vijf zones verdeeld. In de eerste zone zit de diagonaal. Dan volgt het sterrenvenster, waarin een bijzondere reeks paren als regenbogen in elkaar wordt geschoven en waarin in de gaten paren met de afstanden 6 en 8 passen. In het bosvenster zitten paren met zeer grote afstanden, hun partners belanden ver achteraan in een gereserveerd gebied. Daarna komen de restklassen, dus alle overige paren met de afstanden 1 tot en met 12 in blokken. Ten slotte nemen de n−1 randcellen de plaatsen die overblijven.

Waarom werkt het bouwplan pas vanaf n = 119? De bank is bijna op de plaats af vol. Vrij mogen alleen zoveel plaatsen blijven als er randcellen zonder partner zijn, namelijk n−1. Het bouwplan verliest hoogstens 117 plaatsen: 18 in het sterrenvenster, 66 in de blokken, 21 in het bosvenster en 12 bij het overslaan. Het gaat dus op zodra n−1 minstens 118 is. Bij n = 119 zijn er 118 vrije plaatsen en gaan er hoogstens 117 verloren, zodat er één plaats reserve overblijft.

Voor de kleinere groottes heeft een computerprogramma passende zitordes gezocht en als getallenlijst opgeslagen. Deze lijsten heten certificaten. Lean controleert elk certificaat zelf na, in plaats van het zoekprogramma te vertrouwen.

Waarom het bewijs te vertrouwen is: Lean controleert elke stap

Het bewijs is niet alleen opgeschreven, maar regel voor regel door een bewijscontroleur gecontroleerd. Lean is een programmeertaal voor wiskundige bewijzen. Elke gevolgtrekking wordt zo nauwkeurig opgeschreven dat de computer haar kan narekenen. Gaten of een „vanzelfsprekend" bestaan daar niet. Een fout zou de vertaling laten afbreken.

Daarbij wordt Mathlib gebruikt, de grote gemeenschappelijke bibliotheek van reeds gecontroleerde wiskunde voor Lean, bijvoorbeeld voor rekenregels met eindige verzamelingen en sommen. In het voltooide bewijs komt geen enkele „sorry" voor. Zo heet in Lean de plaatsvervanger waarmee een stap voorlopig kan worden overgeslagen. Er is ook geen eigen axioma (een onbewezen basisaanname) en geen vertrouwen in vertaalde programmacode. Lean kan aan het eind opsommen op welke basisaannames een stelling rust. Hier zijn het alleen de drie gebruikelijke waarop vrijwel de hele Mathlib is gebouwd: propext, Classical.choice en Quot.sound.

De Python-programma's die certificaten en bouwplan hebben gevonden, hoeven niet foutloos te zijn. Een onjuist certificaat of een onjuist bouwplan zou door Lean worden afgewezen. Dat is de eigenlijke winst bij het inzetten van AI en zoekprogramma's: de hulpmiddelen mogen raden, de controle blijft toch streng.

Wat een mens moet controleren: de definitie in vijf regels

Een grens geldt voor elk door de computer gecontroleerd bewijs: de definitie aan het begin wordt niet gecontroleerd, maar verondersteld. In dit geval is de definitie maar vijf regels lang, en in alledaagse taal zegt ze dit: er is een vulling van de cellen met gehele getallen. Geen twee cellen dragen dezelfde waarde. De gebruikte waarden zijn precies de getallen van −K tot K. Elke rij in elk van de drie richtingen heeft som 0. In de aangescherpte versie staat bovendien de 0 in het midden.

Drie mogelijke achterdeurtjes zijn uitgesloten. Ten eerste passen cellen en getallen bij elkaar: het zeshoek heeft 3n(n−1)+1 cellen, en van −K tot K zijn er precies zoveel getallen, „elk getal precies één keer" wordt dus afgedwongen. Ten tweede tellen waarden buiten de cellen niet mee, alle voorwaarden hebben alleen betrekking op cellen binnen het zeshoek. Ten derde zijn rijen buiten het zeshoek leeg, hun som is automatisch 0, wat onschuldig is. De formule voor K gebruikt gehele deling, dat is onbedenkelijk omdat n(n−1) altijd even is.

Bij de controle viel bovendien een leemte op die inmiddels is gedicht. De oorspronkelijke definitie eiste de 0 in het midden niet uitdrukkelijk. De constructie levert die weliswaar altijd, omdat gespiegelde cellen tegengestelde waarden dragen. Toch is er nu de aangescherpte definitie met de extra voorwaarde dat het midden 0 is, en de tweede hoofdstelling bewijst haar voor alle n vanaf 3.

Een restvertrouwen blijft, zoals bij elk formeel bewijs. Het betreft de kleine controlekern van Lean en de basisdefinities van Mathlib, bijvoorbeeld voor sommen en intervallen. Gebruikt werd een voorlopige versie van Lean 4. Bovendien liep de controle tot nu toe in één enkele omgeving. Zekerder wordt het als iemand de bestanden onafhankelijk op een eigen computer compileert. Optioneel kan een apart controleprogramma zoals lean4checker de voltooide bewijsbestanden nogmaals narekenen. Voor kleine groottes kan bovendien een concreet zeshoek worden uitgegeven en met de hand worden nagerekend. Dat bewijst niets extra, maar laat aanschouwelijk zien dat de definitie het bedoelde treft.

Cijfers en feiten over het bewijs

Over de uitspraak: bewezen is een magisch zeshoek met som nul voor elke orde n vanaf 3, ook met de 0 in het midden. Kant-en-klare zeshoeken zijn er voor n = 3 tot en met 6. Voor n = 7 tot en met 118 leveren certificaten de oplossing van de basispuzzel, waarvan er 57 nieuw zijn, namelijk die voor n = 62 tot en met 118. Het algemene bouwplan geldt vanaf n = 119, wat overeenkomt met straal 118. Het verliest hoogstens 117 plaatsen en laat bij n = 119 minstens één plaats reserve. De grootste certificaatorde is n = 118, wat overeenkomt met 6.903 cellen in de driehoek.

Over de omvang: de bouwstenen 1 tot en met 4 en de certificaten tot en met n = 61 zijn samengevoegd in één bestand van 2.713 regels. Bouwsteen 5 bestaat uit 40 bestanden met ongeveer 7.000 regels. De grootste geheugenbehoefte ligt bij 5,9 gigabyte, en wel bij een bestand over de eerste rij van het bouwplan. Gebruikt zijn Lean 4 in de voorlopige versie v4.35.0-rc4 en Mathlib. Als axioma's verschijnen alleen propext, Classical.choice en Quot.sound, open gaten zijn er niet.

Over de rekentijd: de herbouw van bouwsteen 5 duurt ongeveer 38 minuten, de certificaten hebben parallel ongeveer 23 minuten nodig. Afzonderlijke bestanden hebben duidelijk langer nodig. Het bestand met de bouwstenen 1 tot en met 4 heeft 460 seconden nodig, het hulpbestand met de formules van de gewenste afstanden 897 seconden, de certificaten voor n = 62 tot en met 89 nog eens 437 seconden en die voor n = 90 tot en met 117 nog eens 927 seconden. De bestanden over de eerste rij hebben samen ongeveer 18 minuten nodig. Deze tijden beschrijven de herbouw van de voltooide controle. Het hele geautomatiseerde bewijstraject met zoeken en ontwikkelen kostte enkele uren.

Over de voortests: het bouwplan werd vóór het Lean-bewijs numeriek getest, als exacte nabootsing van de definities voor de stralen 118 tot en met 450. De hulpuitspraken werden gecontroleerd tot en met straal 20.000. Deze tests waren slechts een voorcontrole, het bewijs zelf is de Lean-tekst.

Hoe het verdergaat: open vragen en plaatsbepaling

Gukovs werk en het Lean-bewijs vullen elkaar aan. Gukov leverde het patroon, de constructie en een schets met de grens 114. De schets rekende de gaten van de eerste rij en van de bossen niet na. Naïef geplaatst zouden daar samen ongeveer 2n tot 3n plaatsen ontbroken hebben, meer dan de toegestane n−1. Het Lean-bewijs zet precies op deze plek in. Het levert formules voor de gewenste afstanden, een pakkingsplan met hoogstens 117 verloren plaatsen in plaats van 2n tot 3n en nieuwe certificaten voor de ordes 62 tot en met 118. Daarmee zijn alle ordes vanaf 3 gedekt.

Open blijft vooralsnog de onafhankelijke controle: een herbouw op een vreemde computer (die de auteur al heeft geleverd), liefst met lean4checker, en een beoordeling door vakmensen. De Lean-bestanden zijn in deze beschrijving nog niet openbaar gelinkt. Bovendien stelt Gukov op zijn pagina een vraag die het bewijs niet beantwoordt: waarom lijken de celwaarden willekeurig, terwijl de bijbehorende potentiaalvelden glad ogen? Verdere varianten van de puzzel zijn denkbaar, beloofd wordt daarover niets.

Een puzzel die begon bij een honingraatfiguur met 19 velden is voor elke grootte opgelost. Daarvoor was eerst het idee van een mens nodig, daarna AI als zoeker en bewijsassistent en ten slotte een controleur die geen van de betrokkenen gelooft, maar elke stap narekent.