Magisk hexagon: hittad med AI för alla storlekar

Bikakepusslet har nu ett svar för varje storlek. Författaren hittade beviset med hjälp av AI, och bevisassistenten Lean kontrollerade det maskinellt; en oberoende granskning återstår. Här förklaras det utan facktermer.

En magisk hexagon är ett sifferpussel som spelas på bikakeceller. Beviset för att sådana hexagoner finns i varje storlek hittades med hjälp av AI och kontrollerades maskinellt av Lean. Den automatiska bevissökningen krävde några timmars datortid. Det som avses här är uttryckligen det matematiska pusslet och inte den likalydande termen från ekonomisk politik.

Artikeln förklarar först vad pusslet kräver och följer vägen från den första hexagonen till beviset. Därefter följer bevisidén i fem byggstenar, var och en med en figur. Slutet handlar om varför man kan lita på ett datorkontrollerat bevis, vad en människa ändå måste kontrollera och vilka siffror och fakta som ligger bakom resultatet.

Magisk hexagon: vad sifferpusslet kräver

Spelplanen är en bikakefigur formad som en regelbunden hexagon. Storleken kallas ordning n och anger hur många celler som ligger på en sida. En hexagon av ordning n består av 3n(n−1)+1 celler. För n = 3 är det 19 celler, för n = 10 redan 271.

Heltal skrivs in i cellerna så att varje rak rad har samma summa. Raderna räknas i alla tre riktningar i bikakefiguren. I varje riktning finns 2n−1 rader. De kortaste vid kanten har n celler, den mittersta har 2n−1 celler.

Den mest kända magiska hexagonen har talen 1 till 19 och ordning 3. Varje rad har summan 38. Det är den klassiska hexagonen, och för tal som börjar vid 1 är det den enda storlek där pusslet går ihop. Ett enkelt delbarhetsresonemang visar att den nödvändiga radsumman bara är ett heltal för n = 1 och n = 3. För alla andra ordningar misslyckas alltså den klassiska varianten redan från början.

Därför kretsar det nya arbetet kring en besläktad variant. I stället för att börja vid 1 används heltalen från −K till K, vart och ett exakt en gång. Här är K = 3n(n−1)/2. För n = 3 är det talen −9 till 9, för n = 10 talen −135 till 135. Varje rad har summan 0, och 0 står i mitten.

Pusslet låter oskyldigt men är svårt. Antalet möjliga ifyllningar växer så snabbt med n att det inte hjälper att prova dem på en dator. Det som behövdes var därför en ritning som fungerar för varje storlek, och ett bevis för att ritningen verkligen alltid går ihop.

Från pusslet 1887 till den största kända hexagonen: historien

Det ursprungliga problemet kommer från Ernst von Haselberg och dateras vanligen till 1887. Några källor anger 1888; originalkällan har inte konsulterats. Senare återupptäckte Adams enligt egen uppgift den klassiska hexagonen 1957 och gjorde den känd genom Martin Gardners spalt. Att denna lösning är den enda, bortsett från rotation och spegling, bevisades av Charles W. Trigg och publicerades 1964. En samling om detta förvaras av Universität Bielefeld, och en översikt finns hos Wolfram MathWorld.

Varianten med på varandra följande heltal och summan 0 kom i blickfånget senare. Mellan 2004 och 2006 hittades ordningarna 4 till 8, ordning 6 i oktober 2004, ordningarna 7 och 8 år 2006. Fram till 2006 var bara ordning 8 känd som största lösning. Mindre ordningar var redan lösta då. En översikt med källor ges av den tyska Wikipedia, vars uppgifter delvis saknar belägg.

År 2024 hittade Dr. DSGVO, författaren till den här bloggen, en lösning av ordning 9 med AI. Då var det den största kända lösningen.

Den 2 augusti 2026 publicerade Konstantin Gukov sedan ett mönster på sin sida New magic hexagons. Han sökte lösningar upp till ordning 21 och insåg att en konstruktionsregel för godtyckligt stora hexagoner sannolikt kan härledas ur dem. Gukov beskrev en algoritm och en bevisskiss som skulle gälla från ordning 114. Han påpekar själv att skissen inte är formaliserad i Lean och inte oberoende kontrollerad. Beviset saknades alltså fortfarande.

För detta gap finns nu ett bevis för alla ordningar från 3. Det togs fram med AI och dokumenteras i en beskrivning daterad den 21 oktober 2026. Det är maskinellt kontrollerat av Lean, en oberoende granskning återstår, och Lean-filerna är ännu inte länkade offentligt. Mer om det längre fram.

Magiska hexagoner för alla storlekar: vad som är bevisat

Det som är bevisat: för varje ordning n från 3 finns en magisk hexagon med talen från −K till K där varje rad i alla tre riktningar har summan 0. Den skärpta versionen, där 0 dessutom står i mitten, är också bevisad. Det finns ingen övre gräns. Gukovs skiss gäller först från ordning 114; ordningarna dessförinnan förblev öppna utan den sista byggstenen.

Täckningen är uppdelad i steg. Ordning 2 är omöjlig eftersom de sju talen −3 till 3 inte kan fördelas lämpligt. Den delen ingår inte i Lean-beviset. För ordningarna 3 till 6 finns färdiga hexagoner som Lean kontrollräknade tal för tal. För ordningarna 7 till 61 gäller en allmän ritning, kompletterad med en kontrollerad lösning av ett delpussel vardera. För ordningarna 62 till 118 gäller detsamma, med den skillnaden att de nödvändiga listorna räknades om och kontrollerades. Från ordning 119 räcker en fast ritning som är bevisad i allmänhet för varje n.

Två huvudsatser sammanfattar detta. Den första säger att det för varje n från 3 finns en magisk hexagon av ordning n. Den andra säger detsamma för den skärpta versionen med 0 i mitten. Båda satserna har inget annat antagande än n ≥ 3.

Beviset i fem byggstenar: översikt

Beviset kan föreställas som en stege. Varje byggsten krymper uppgiften tills bara en bänkplacering återstår. Byggstenarna 1 till 4 fanns redan i kontrollerad form. Nytt är den femte byggstenen, placeringsplanen för varje storlek. Den fullbordar beviset.

Följande avsnitt går igenom byggstenarna i ordning. De tre första är intuitiva, de två sista kan vara lite mer tekniska. Alla beräkningar kontrollerades av Lean, så idéerna räcker i texten.

Byggsten 1: en sjättedel räcker, för motstående cell håller det negativa talet

Hela hexagonen behöver inte planeras, en sjättedel räcker. Varje cell har en motstående cell som ligger spegelvänd genom mitten. Om talet a står i en cell, hamnar −a i den motstående cellen. Därmed används varje tal tillsammans med sitt negativa, och 0 blir över till mitten.

Detta får en praktisk följd för raderna. Den speglade raden har exakt den negativa summan. Om en rad är balanserad är därmed även dess spegelbild det. Rader genom mitten är balanserade automatiskt.

Hexagonen delas i sex lika stora trianglar kring mitten. Tre av dem är trianglar med motstående celler: deras tal följer av speglingen genom mitten med omvänt tecken. Ytterligare två är kopior av den sjätte triangeln, vridna 120 grader, och får närbesläktade tal. Kvar blir en enda fri triangel med T = n(n−1)/2 celler. För n = 10 är det 45 i stället för 271 celler.

Villkoret att varje rad har summan 0 blir därmed ett villkor på denna triangel. För varje rad ska en viktad summa av dess poster vara noll. Den summan kallas i det följande radens balans.

Byggsten 2: varje tal blir bas plus siffra

I det andra steget delas varje tal i två delar, en bas och en siffra. Båda delarna balanseras var för sig. Eftersom radsummor helt enkelt adderas när tal adderas är hexagonen magisk så snart båda delarna är balanserade för sig.

För detta delas förrådet av tal 1 till 3T i grupper om tre: k, T+k och 2T+k för k från 1 till T. Varje grupp är basen T+k plus T gånger en siffra, där siffran är −1, 0 eller 1. För hexagonen av ordning 3 är T = 3 och förrådet går från 1 till 9. Bas 4 ger 1, 4 och 7, bas 5 ger 2, 5 och 8, bas 6 ger 3, 6 och 9.

Uppgiften faller därmed isär i två oberoende pussel. Det första är ett siffrefält av −1, 0 och 1 med balansen noll i varje rad. Det andra är ett basfält där beloppen T+1 till 2T fördelas och förses med tecken så att balansen i varje rad blir noll.

Byggsten 3: siffrefältet växer som en stege

Siffrefältet är fullständigt löst för varje ordning från n = 5, genom induktion i steg om tre. Principen känner alla från en stege: den som har det första trappsteget och en regel för steget till nästa når varje trappsteg.

Först finns färdiga, balanserade siffrefält för radierna 4, 5 och 6. Radien är n−1. Sedan gäller en utvidgningsregel: ett balanserat siffrefält kan utvidgas med tre nya lager vid kanten. De nya lagren mönstras så att de tar ut varandra i varje rad. Från 4 leder det till 7, 10, 13 och vidare, från 5 till 8, 11 och vidare, från 6 till 9, 12 och vidare. Därmed nås varje radie från 4.

Den här delen kostar knappt någon datortid vid kontrollen. Den löser dock bara det första av de två delpusslen; basfältet återstår.

Byggsten 4: målavstånd som balanserar varandra

Basfältet söks inte direkt. I stället fastställs först för varje cellpar hur mycket de två baserna ska skilja sig åt. Dessa målavstånd är bevisade i allmänhet för alla ordningar från n = 13.

Nästan alla celler i triangeln bildar par som ligger spegelvända kring dess mittaxel. En cell i ett par får ett minus, den andra ett plus. I balansen återstår bara skillnaden mellan de två beloppen; den gemensamma delen T faller bort. Det enda som spelar roll är alltså avståndet mellan de två rangerna. Rangen är helt enkelt platsnumret: basen T+k har rang k.

Målavstånden uppstår i flera steg. Det finns associativitetskretsar: små mönster av fyra cellpar med vikterna +1 och −1 och balansen noll i varje rad. Namnet kommer från den räkneregel som säger att parenteser i summor kan flyttas utan att resultatet ändras. Varje summa av sådana mönster har också balansen noll. Av många mönster uppstår ett huvudfält där inget cellpar får avståndet 0. Ett avstånd på 0 vore oanvändbart, eftersom två celler aldrig får bära samma tal.

Cellerna på mittaxeln har ingen partner. De får de lägsta rangerna 1, 2, 3 och så vidare, och huvudfältet balanserar exakt deras bidrag. De diagonala cellerna bär dessutom andelen T, som inte tar ut sig själv. Den balanseras av två förgrenade kedjor av cellpar, skogarna. Deras avstånd förstoras med ungefär T/2, tillsammans alltså med T.

Resultatet är en fullständig uppsättning målavstånd med balansen noll i varje rad, och inget av dem är noll. De flesta avstånd är små och ligger på högst 12. Cellerna i den första raden har avstånd upp till ungefär 2n, skogarnas par avstånd nära T/2.

Byggsten 5: placeringsplanen för varje storlek

Till sist måste rangerna 1 till T faktiskt fördelas så att varje cellpar får exakt sitt målavstånd. Från n = 119 görs det med en fast ritning; under det med listor som hittats av dator och kontrollerats av Lean.

Det kan föreställas som en placeringsplan på en lång bänk med T platser. De diagonala cellerna sitter på fasta platser på de första platserna 1, 2, 3 och så vidare. Varje cellpar behöver två platser på föreskrivet avstånd. Ingen plats får vara upptagen två gånger. Exakt n−1 platser förblir lediga. De går till kantcellerna utan partner, för vilka vilken plats som helst duger.

Det avgörande tricket är block. Par med samma avstånd g kan staplas utan luckor. För g = 3 fyller paren (1, 4), (2, 5) och (3, 6) platserna 1 till 6 utan lucka. I allmänhet fyller g par med avstånd g exakt 2g på varandra följande platser, därefter följer nästa block. På så sätt slösar varje avståndsgrupp högst g−1 platser i slutet av sitt sista block. Grupperna med avstånden 1 till 12 kostar tillsammans högst 0+1+…+11 = 66 platser.

Bänken delas från främre till bakre änden i fem zoner. I den första zonen sitter diagonalen. Därefter kommer stjärnfönstret, där en särskild rad av par är nästlade som regnbågar och par med avstånden 6 och 8 passar in i luckorna. I skogsfönstret sitter par med mycket stora avstånd, vars partner hamnar långt bak i ett reserverat område. Sedan kommer restklasserna, alltså alla återstående par med avstånden 1 till 12 i block. Till sist tar de n−1 kantcellerna de platser som är kvar.

Varför fungerar ritningen först från n = 119? Bänken är nästan exakt full. Bara så många platser får stå lediga som det finns kantceller utan partner, nämligen n−1. Ritningen förlorar högst 117 platser: 18 i stjärnfönstret, 66 i blocken, 21 i skogsfönstret och 12 vid överhoppning. Det går alltså ihop så snart n−1 är minst 118. Vid n = 119 är 118 platser lediga och högst 117 går förlorade, så en plats reserv återstår.

För de mindre storlekarna sökte ett datorprogram efter lämpliga placeringsplaner och sparade dem som talslistor. Dessa listor kallas certifikat. Lean kontrollerar varje certifikat själv på nytt i stället för att lita på sökprogrammet.

Varför man kan lita på beviset: Lean kontrollerar varje steg

Beviset är inte bara nedskrivet utan kontrollerat rad för rad av en bevisgranskare. Lean är ett programmeringsspråk för matematiska bevis. Varje slutledning skrivs ned så exakt att datorn kan räkna om den. Det finns inga luckor och inget "uppenbarligen". Ett fel skulle få översättningen att avbrytas.

Det använder Mathlib, det stora gemensamma biblioteket av redan kontrollerad matematik för Lean, till exempel för räkneregler med ändliga mängder och summor. Inte ett enda "sorry" förekommer i det färdiga beviset. Så heter platshållaren i Lean med vilken ett steg tillfälligt kan hoppas över. Det finns heller inget eget axiom (ett obevisat grundantagande) och inget förtroende för översatt programkod. Till slut kan Lean lista vilka grundantaganden en sats vilar på. Här finns bara de tre vanliga som praktiskt taget hela Mathlib bygger på: propext, Classical.choice och Quot.sound.

Python-programmen som hittade certifikaten och ritningen behöver inte vara felfria. Ett felaktigt certifikat eller en felaktig ritning skulle avvisas av Lean. Det är den verkliga vinsten med att använda AI och sökprogram: verktygen får gissa, kontrollen är ändå sträng.

Vad en människa måste kontrollera: definitionen i fem rader

En gräns gäller för varje datorkontrollerat bevis: definitionen i början kontrolleras inte utan antas. I det aktuella fallet är definitionen bara fem rader lång, och på vardagsspråk säger den detta: det finns en ifyllning av cellerna med heltal. Inga två celler har samma värde. De värden som används är exakt talen från −K till K. Varje rad i var och en av de tre riktningarna har summan 0. I den skärpta versionen står 0 dessutom i mitten.

Tre möjliga kryphål är uteslutna. För det första stämmer celler och tal överens: hexagonen har 3n(n−1)+1 celler, och från −K till K finns exakt lika många tal, så "varje tal exakt en gång" är tvingande. För det andra räknas värden utanför hexagonen inte; alla villkor avser bara celler inom hexagonen. För det tredje är rader utanför hexagonen tomma, deras summa är automatiskt 0, vilket är ofarligt. Formeln för K använder heltalsdivision, vilket är oproblematiskt eftersom n(n−1) alltid är jämnt.

Kontrollen avslöjade också en lucka som sedan dess har täppts till. Den ursprungliga definitionen krävde inte uttryckligen 0 i mitten. Konstruktionen levererar det alltid, eftersom speglade celler bär motsatta värden. Ändå finns nu den skärpta definitionen med tilläggsvillkoret att mitten är 0, och den andra huvudsatsen bevisar den för alla n från 3.

Ett visst kvarstående förtroende behövs, som vid varje formellt bevis. Det gäller Leans lilla kärna och Mathlibs grunddefinitioner, till exempel för summor och intervall. En förhandsversion av Lean 4 användes. Dessutom har kontrollen hittills körts i en enda miljö. Det blir säkrare när någon oberoende kompilerar filerna på sin egen maskin. Som tillval kan ett separat kontrollprogram som lean4checker verifiera de färdiga bevisfilerna ännu en gång. För små storlekar kan också en konkret hexagon skrivas ut och räknas om för hand. Det bevisar inget ytterligare, men visar åskådligt att definitionen fångar det som avses.

Siffror och fakta om beviset

Om påståendet: en magisk hexagon med summan noll är bevisad för varje ordning n från 3, även med 0 i mitten. Färdiga hexagoner finns för n = 3 till 6. För n = 7 till 118 levererar certifikat lösningen av baspusslet, varav 57 är nya, nämligen de för n = 62 till 118. Den allmänna ritningen gäller från n = 119, vilket motsvarar radie 118. Den förlorar högst 117 platser och lämnar minst en plats reserv vid n = 119. Den största certifikatordningen är n = 118, vilket motsvarar 6 903 celler i triangeln.

Om storleken: byggstenarna 1 till 4 och certifikaten upp till n = 61 är sammanfattade i en fil som har 2 713 rader. Byggsten 5 består av 40 filer med omkring 7 000 rader. Det största minnesbehovet är 5,9 gigabyte, för en fil om den första raden i ritningen. Lean 4 i förhandsversionen v4.35.0-rc4 och Mathlib användes. Bara propext, Classical.choice och Quot.sound förekommer som axiom, och det finns inga öppna luckor.

Om datortiden: att bygga om byggsten 5 tar ungefär 38 minuter, och certifikaten behöver omkring 23 minuter parallellt. Enskilda filer tar betydligt längre. Filen med byggstenarna 1 till 4 behöver 460 sekunder, hjälpfilen med formlerna för målavstånden 897 sekunder, certifikaten för n = 62 till 89 ytterligare 437 sekunder och de för n = 90 till 117 ytterligare 927 sekunder. Filerna om den första raden tar tillsammans omkring 18 minuter. Dessa tider beskriver ombyggnaden av den färdiga kontrollen. Hela den automatiserade bevisinsatsen, med sökning och utveckling, tog några timmar.

Om förtesterna: före Lean-beviset testades ritningen numeriskt som en exakt kopia av definitionerna för radierna 118 till 450. Hjälpsatserna kontrollerades upp till radie 20 000. Dessa tester var bara en förkontroll; beviset i sig är Lean-texten.

Vad som kommer härnäst: öppna frågor och sammanhang

Gukovs arbete och Lean-beviset kompletterar varandra. Gukov levererade mönstret, konstruktionen och en skiss med gränsen 114. Skissen räknade inte om luckorna i den första raden och i skogarna. Naivt satta skulle omkring 2n till 3n platser ha saknats där tillsammans, mer än de tillåtna n−1. Lean-beviset börjar på exakt den punkten. Det levererar formler för målavstånden, en packningsplan med högst 117 förlorade platser i stället för 2n till 3n, och nya certifikat för ordningarna 62 till 118. Därmed är alla ordningar från 3 täckta.

Det som tills vidare förblir öppet är den oberoende kontrollen: en ombyggnad på en främmande maskin (redan tillhandahållen av författaren), helst med lean4checker, och en granskning av experter. Lean-filerna är ännu inte länkade offentligt i denna beskrivning. Dessutom ställer Gukov en fråga på sin sida som beviset inte besvarar: varför ser cellernas värden slumpmässiga ut medan de tillhörande potentialfälten ser jämna ut? Ytterligare varianter av pusslet är tänkbara, men inget utlovas.

Ett pussel som började med en bikakefigur av 19 celler är löst för varje storlek. Det krävde först en människas idé, sedan AI som sökare och bevisassistent, och till sist en kontrollant som inte tror på någon av de inblandade utan räknar om varje steg.