Magisk sekskant: Fundet med AI for enhver størrelse

Bikubepuslespillet har nu et svar for enhver størrelse. Forfatteren fandt beviset ved hjælp af AI, og bevisprogrammet Lean har kontrolleret det maskinelt, en uafhængig fagfællebedømmelse mangler endnu. Her forklares det uden fagsprog.

En magisk sekskant er et talpuslespil, der spilles på bikubefelter. Beviset for, at der findes sådanne sekskanter i enhver størrelse, blev fundet ved hjælp af AI og kontrolleret maskinelt af Lean. Den automatiserede bevisførelse kostede nogle timers regnetid. Der menes udtrykkeligt det matematiske puslespil og ikke det tilsvarende begreb fra økonomisk politik.

Indlægget forklarer først, hvad puslespillet kræver, og følger forløbet fra den første sekskant til beviset. Derefter kommer bevisidéen i fem byggesten, hver med et billede. Til sidst handler det om, hvorfor man kan stole på et computerkontrolleret bevis, hvad et menneske alligevel skal kontrollere, og hvilke tal og fakta der ligger bag resultatet.

Magisk sekskant: Hvad talpuslespillet kræver

Spillefladen er en bikubefigur i form af en regulær sekskant. Størrelsen kaldes orden n og angiver, hvor mange celler der ligger på en side. En sekskant af orden n består af 3n(n−1)+1 celler. Ved n = 3 er det 19 celler, ved n = 10 allerede 271.

I cellerne skrives hele tal, og det sker på en sådan måde, at hver ret række giver den samme sum. Der tælles rækker i alle tre retninger af bikubefiguren. I hver retning er der 2n−1 rækker. De korteste ved kanten har n celler, den midterste har 2n−1 celler.

Den mest berømte magiske hexagon indeholder tallene fra 1 til 19 og har orden 3. Hver række giver 38. Det er den klassiske sekskant, og for tal fra 1 og opefter findes der kun denne ene størrelse, hvor puslespillet går op. En enkel overvejelse om delelighed viser, at den nødvendige rækkesum kun bliver et helt tal ved n = 1 og n = 3. For alle andre ordener strander den klassiske variant altså allerede i udgangspunktet.

Derfor handler det nye arbejde om en beslægtet variant. I stedet for at begynde ved 1 bruges de hele tal fra −K til K, hvert netop én gang. Her er K = 3n(n−1)/2. Ved n = 3 er det tallene −9 til 9, ved n = 10 tallene −135 til 135. Hver række giver 0, og i midten står 0.

Puslespillet lyder uskyldigt, men er svært. Antallet af mulige udfyldninger vokser så hurtigt med n, at det ikke fører vidt at prøve sig frem på en computer. Det, man søgte, var derfor en byggeplan, der virker for enhver størrelse, og et bevis for, at byggeplanen virkelig altid går op.

Fra puslespillet i 1887 til den største kendte hexagon: forløbet

Det oprindelige problem stammer fra Ernst von Haselberg og dateres som regel til 1887. Enkelte kilder nævner 1888, primærkilden er ikke gennemgået. Senere genfandt Adams efter egen beretning den klassiske sekskant i 1957 og gjorde den kendt gennem Martin Gardners klumme. At denne løsning er den eneste, bortset fra drejning og spejling, blev bevist af Charles W. Trigg, offentliggjort i 1964. En samling om emnet føres af Universitetet i Bielefeld, og et overblik findes hos Wolfram MathWorld.

Varianten med på hinanden følgende hele tal og sum 0 kom først senere i fokus. Mellem 2004 og 2006 blev ordenerne 4 til 8 fundet, orden 6 i oktober 2004, ordenerne 7 og 8 i 2006. Frem til 2006 var kun orden 8 kendt som største løsning. Mindre ordener var dengang allerede løst. Et overblik med kildehenvisninger giver den tyske Wikipedia, hvis datoangivelser delvis mangler dokumentation.

I 2024 fandt Dr. DSGVO, bloggens forfatter, en løsning af orden 9 ved hjælp af AI. Det var dengang den største kendte løsning.

Den 2. august 2026 offentliggjorde Konstantin Gukov så et mønster på sin side New magic hexagons. Han søgte løsninger op til orden 21 og indså, at der sandsynligvis kan udledes en konstruktionsforskrift for vilkårligt store sekskanter. Gukov beskrev en algoritme og en bevisskitse, der til sidst skulle tage fat fra orden 114. Han påpeger selv, at denne skitse ikke er formaliseret i Lean og ikke uafhængigt kontrolleret. Beviset manglede altså stadig.

For dette hul foreligger der nu et bevis for alle ordener fra 3. Det blev til med AI og er dokumenteret som en beskrivelse fra den 21. oktober 2026. Lean har kontrolleret det maskinelt, en uafhængig fagfællebedømmelse mangler endnu, og Lean-filerne er endnu ikke linket offentligt. Mere om det senere.

Magiske sekskanter i alle størrelser: Hvad der er bevist

Det er bevist, at der for enhver orden n fra 3 findes en magisk sekskant med tallene fra −K til K, hvor hver række i alle tre retninger har sum 0. Også den skærpede udgave er bevist, hvor 0 desuden står i midten. Der er ingen øvre grænse. Gukovs skitse tager først fat fra orden 114, ordenerne før den forblev åbne uden den sidste byggesten.

Dækningen er trinvis. Orden 2 er umulig, fordi de syv tal −3 til 3 ikke kan fordeles passende. Denne del hører ikke med til Lean-beviset. For ordenerne 3 til 6 foreligger der færdige sekskanter, som Lean har efterprøvet tal for tal. For ordenerne 7 til 61 tager en generel byggeplan fat, suppleret med en kontrolleret løsning af et delpuslespil for hver orden. For ordenerne 62 til 118 gælder det samme, blot er de nødvendige lister nyberegnet og kontrolleret. Fra orden 119 er en fast byggeplan nok, som er bevist generelt for ethvert n.

To hovedsætninger opsummerer det. Den første siger, at der for ethvert n fra 3 findes en magisk hexagon af orden n. Den anden siger det samme for den skærpede udgave med 0 i midten. Begge sætninger har ingen forudsætning ud over n ≥ 3.

Beviset i fem byggesten: Overblik

Beviset kan forestilles som en stige. Hver byggesten gør opgaven mindre, indtil der til sidst kun er en siddeplan på en bænk tilbage. Byggestenene 1 til 4 forelå allerede kontrolleret. Ny er den femte byggesten, siddeplanen for enhver størrelse. Den afslutter beviset.

De følgende afsnit gennemgår byggestenene efter tur. De første tre er anskuelige, de sidste to må gerne være lidt mere tekniske. Alle beregninger er kontrolleret af Lean, så i teksten er idéerne nok.

Byggesten 1: En sjettedel er nok, for overfor står det negative

Hele sekskanten behøver ikke at blive planlagt, en sjettedel rækker. Hver celle har en modcelle, der ligger spejlet i midtpunktet. Står tallet a i en celle, kommer −a i modcellen. Dermed er hvert tal brugt sammen med sit negative, og 0 er tilbage til midten.

Det har en praktisk følge for rækkerne. Den spejlede række har netop den negative sum. Er en række afbalanceret, er dens spejlbillede det også. Rækker gennem midten er endda afbalancerede af sig selv.

Sekskanten falder omkring midten i seks ens trekanter. Tre af dem er modcelle-trekanter: Deres tal følger af spejlingen gennem midten med omvendt fortegn. To andre er kopier af den sjette trekant drejet 120 grader og får nært beslægtede tal. Tilbage er en enkelt fri trekant med T = n(n−1)/2 celler. Ved n = 10 er det 45 i stedet for 271 celler.

Betingelsen "hver række har sum 0" bliver dermed til en betingelse for denne trekant. For hver række skal en vægtet sum af dens indgange give nul. Denne sum kaldes i det følgende rækkens balance.

Byggesten 2: Hvert tal bliver til basis plus ciffer

I det andet trin opdeles hvert tal i to dele, en basis og et ciffer. Begge dele afbalanceres hver for sig. Fordi rækkesummer blot lægges sammen ved addition, er sekskanten magisk, så snart begge dele hver for sig er afbalancerede.

Talforrådet 1 til 3T deles hertil i grupper på tre: k, T+k og 2T+k for k fra 1 til T. Hver gruppe er basis T+k plus T gange et ciffer, hvor cifferet er −1, 0 eller 1. Ved sekskanten af orden 3 er T = 3, og forrådet går fra 1 til 9. Basis 4 giver 1, 4 og 7, basis 5 giver 2, 5 og 8, basis 6 giver 3, 6 og 9.

Dermed falder opgaven i to uafhængige puslespil. Det første er et cifferfelt af −1, 0 og 1 med balance nul i hver række. Det andet er et basisfelt, hvor beløbene T+1 til 2T fordeles og forsynes med fortegn, så balancen i hver række bliver nul.

Byggesten 3: Cifferfeltet vokser som en stige

Cifferfeltet er fuldstændigt løst for enhver orden fra n = 5, og det sker ved induktion i trin på tre. Princippet kender enhver stige: Den, der har det første trin og en regel for skridtet til det næste, når ethvert trin.

Først er der færdige, afbalancerede cifferfelter for radius 4, 5 og 6. Radius er her n−1. Så gælder en tilbygningsregel: Et afbalanceret cifferfelt kan udvides med tre nye lag ved kanten. De nye lag er mønstret på en sådan måde, at de ophæver hinanden i hver række. Fra 4 går det således til 7, 10, 13 og videre, fra 5 til 8, 11 og videre, fra 6 til 9, 12 og videre. Dermed nås enhver radius fra 4.

Denne del koster næsten ingen regnetid ved kontrollen. Den løser dog kun det første af de to delpuslespil, basisfeltet er stadig åbent.

Byggesten 4: Ønskeafstande, der udligner hinanden

Basisfeltet søges ikke direkte. I stedet fastlægges først for hvert cellepar, hvor meget de to baser skal adskille sig. Disse ønskeafstande er generelt bevist for alle ordener fra n = 13.

Næsten alle celler i trekanten danner par, der ligger spejlet om dens midterakse. Den ene celle i et par får et minus, den anden et plus. I balancen er det så kun forskellen mellem de to beløb, der er tilbage, den fælles andel T falder væk. Det kommer altså kun an på afstanden mellem de to rang. Rangen er blot pladsnummeret: Basis T+k har rang k.

Ønskeafstandene opstår i flere trin. Der er associativitetskredse: små mønstre af fire cellepar med vægtene +1 og −1 og balance nul i hver række. Navnet stammer fra regnereglen om, at parenteser i summer kan flyttes uden at ændre resultatet. Hver sum af sådanne mønstre har også balance nul. Af mange mønstre opstår et masterfelt, hvor intet cellepar får afstanden 0. En afstand på 0 ville være ubrugelig, fordi to celler aldrig må bære det samme tal.

Cellerne på midteraksen har ingen partner. Disse får de mindste rang 1, 2, 3 og så videre, og masterfeltet udligner netop deres bidrag. Diagonalcellerne bærer desuden andelen T, som ikke forsvinder. Den udligner to forgrenede kæder af cellepar, skovene. Deres afstande forøges med omkring T/2, tilsammen altså med T.

Resultatet er et fuldstændigt sæt ønskeafstande med balance nul i hver række, og ingen af dem er nul. De fleste afstande er små og ligger på højst 12. Cellerne i første række har afstande op til omkring 2n, parrene i skovene afstande tæt på T/2.

Byggesten 5: Siddeplanen for enhver størrelse

Til sidst skal rang 1 til T virkelig fordeles, så hvert cellepar får netop sin ønskeafstand. Fra n = 119 sker det med en fast byggeplan, derunder med lister, som computeren har fundet og Lean har kontrolleret.

Det kan forestilles som en siddeplan på en lang bænk med T pladser. Diagonalcellerne sidder fast på de første pladser 1, 2, 3 og så videre. Hvert cellepar har brug for to pladser i den foreskrevne afstand. Ingen plads må være dobbeltbesat. Netop n−1 pladser forbliver ledige. De går til randcellerne uden partner, og for dem er enhver plads god nok.

Det afgørende trick er blokke. Par med samme afstand g kan stables uden huller. Ved g = 3 fylder parrene (1, 4), (2, 5) og (3, 6) pladserne 1 til 6 uden hul. Generelt fylder g par med afstand g netop 2g på hinanden følgende pladser, derefter følger den næste blok. Dermed spilder hver afstandsgruppe højst g−1 pladser for enden af sin sidste blok. Grupperne med afstandene 1 til 12 koster tilsammen højst 0+1+…+11 = 66 pladser.

Bænken deles forfra og bagud i fem zoner. I den første zone sidder diagonalen. Så følger stjernevinduet, hvor en særlig række af par skubbes ind i hinanden som regnbuer, og i hullerne passer par med afstandene 6 og 8. I skovvinduet sidder par med meget store afstande, deres partnere havner langt bagude i et reserveret område. Derefter kommer restklasserne, altså alle øvrige par med afstandene 1 til 12 i blokke. Til sidst tager de n−1 randceller de pladser, der er tilbage.

Hvorfor tager byggeplanen først fat fra n = 119? Bænken er næsten præcis fuld. Der må kun forblive så mange pladser ledige, som der er randceller uden partner, nemlig n−1. Byggeplanen taber højst 117 pladser: 18 i stjernevinduet, 66 i blokkene, 21 i skovvinduet og 12 ved overspringning. Den går altså op, så snart n−1 er mindst 118. Ved n = 119 er 118 pladser ledige, og højst 117 går tabt, så der er en plads i reserve.

For de mindre størrelser har et computerprogram søgt passende siddeplaner og gemt dem som talliste. Disse lister kaldes certifikater. Lean efterprøver hvert certifikat selv i stedet for at stole på søgeprogrammet.

Hvorfor man kan stole på beviset: Lean kontrollerer hvert trin

Beviset er ikke blot skrevet ned, men kontrolleret linje for linje af en bevisprøver. Lean er et programmeringssprog til matematiske beviser. Hver slutning nedskrives så nøjagtigt, at computeren kan efterregne den. Huller eller et "oplagt" findes der ikke. En fejl ville få oversættelsen til at afbryde.

Her bruges Mathlib, det store fælles bibliotek af allerede kontrolleret matematik til Lean, for eksempel til regneregler for endelige mængder og summer. I det færdige bevis forekommer ikke et eneste "sorry". Sådan hedder i Lean pladsholderen, der midlertidigt lader et trin springe over. Der er heller intet eget aksiom (en ubevist grundantagelse) og ingen tillid til oversat programkode. Lean kan til sidst opliste, hvilke grundantagelser en sætning hviler på. Her er det kun de tre sædvanlige, som stort set hele Mathlib bygger på: propext, Classical.choice og Quot.sound.

De Python-programmer, der har fundet certifikater og byggeplan, behøver ikke være fejlfri. Et forkert certifikat eller en forkert byggeplan ville blive afvist af Lean. Det er den egentlige gevinst ved at bruge AI og søgeprogrammer: Værktøjerne må gætte, kontrollen er alligevel streng.

Hvad et menneske skal kontrollere: Definitionen i fem linjer

En grænse gælder for ethvert computerkontrolleret bevis: Definitionen i begyndelsen kontrolleres ikke, men forudsættes. I det foreliggende tilfælde er definitionen kun fem linjer lang, og i dagligdags sprog siger den dette: Der findes en udfyldning af cellerne med hele tal. Ingen to celler bærer den samme værdi. De anvendte værdier er netop tallene fra −K til K. Hver række i hver af de tre retninger har sum 0. I den skærpede udgave står 0 desuden i midten.

Tre mulige smuthuller er udelukket. For det første passer celler og tal sammen: Sekskanten har 3n(n−1)+1 celler, og fra −K til K er der netop så mange tal, så "hvert tal netop én gang" er altså tvunget. For det andet tæller værdier uden for bikuben ikke, alle betingelser vedrører kun celler i sekskanten. For det tredje er rækker uden for bikuben tomme, deres sum er automatisk 0, hvilket er harmløst. Formlen for K bruger heltalsdivision, det er uproblematisk, fordi n(n−1) altid er lige.

Ved kontrollen faldt der desuden et hul i øjnene, som nu er lukket. Den oprindelige definition krævede ikke udtrykkeligt 0 i midten. Konstruktionen leverer den vel altid, fordi spejlede celler bærer modsatte værdier. Alligevel findes der nu den skærpede definition med tillægsbetingelsen, at midten er 0, og den anden hovedsætning beviser den for alle n fra 3.

En restsikkerhed består, som ved ethvert formelt bevis. Den vedrører Leans lille kontrolkerne og Mathlibs grunddefinitioner, for eksempel til summer og intervaller. Der blev anvendt en forhåndsversion af Lean 4. Desuden foregik kontrollen hidtil i et enkelt miljø. Det bliver sikrere, hvis nogen oversætter filerne uafhængigt på sin egen computer. Valgfrit kan et separat kontrolprogram som lean4checker efterprøve de færdige bevisfiler endnu en gang. For små størrelser kan man desuden udskrive en konkret sekskant og efterregne den i hånden. Det beviser ikke noget ekstra, men viser anskueligt, at definitionen rammer det tilsigtede.

Tal og fakta om beviset

Om udsagnet: Bevist er en magisk hexagon med sum nul for enhver orden n fra 3, også med 0 i midten. Færdige hexagoner findes for n = 3 til 6. For n = 7 til 118 leverer certifikater løsningen af basispuslespillet, heraf er 57 nye, nemlig dem for n = 62 til 118. Den generelle byggeplan gælder fra n = 119, hvilket svarer til radius 118. Den taber højst 117 pladser og lader ved n = 119 mindst en plads i reserve. Den største certifikatorden er n = 118, hvilket svarer til 6.903 celler i trekanten.

Om omfanget: Byggestenene 1 til 4 og certifikaterne til og med n = 61 er samlet i en fil, der omfatter 2.713 linjer. Byggesten 5 består af 40 filer med omkring 7.000 linjer. Det største lagerforbrug er 5,9 gigabyte, og det gælder en fil til byggeplanens første række. Der blev anvendt Lean 4 i forhåndsversionen v4.35.0-rc4 og Mathlib. Som aksiomer optræder kun propext, Classical.choice og Quot.sound, åbne huller er der ingen af.

Om regnetiden: Genopbygningen af byggesten 5 tager omkring 38 minutter, certifikaterne kræver parallelt omkring 23 minutter. Enkelte filer tager markant længere. Filen med byggestenene 1 til 4 kræver 460 sekunder, hjælpefilen med formlerne til ønskeafstandene 897 sekunder, certifikaterne for n = 62 til 89 yderligere 437 sekunder og dem for n = 90 til 117 yderligere 927 sekunder. Filerne til den første række kræver tilsammen omkring 18 minutter. Disse tider beskriver genopbygningen af den færdige kontrol. Den samlede automatiserede bevisførelse med søgning og udvikling kostede nogle timer.

Om forprøverne: Byggeplanen blev testet numerisk før Lean-beviset, som en nøjagtig efterbygning af definitionerne for radius 118 til 450. Hjælpeudsagnene blev kontrolleret op til radius 20.000. Disse tests var kun en forprøve, selve beviset er Lean-teksten.

Hvordan det går videre: åbne spørgsmål og placering

Gukovs arbejde og Lean-beviset supplerer hinanden. Gukov leverede mønsteret, konstruktionen og en skitse med grænsen 114. Skitsen nåede ikke at efterregne hullerne i første række og i skovene. Naivt opstillet ville der der tilsammen have manglet omkring 2n til 3n pladser, mere end de tilladte n−1. Lean-beviset sætter ind netop her. Det leverer formler til ønskeafstandene, en pakkeplan med højst 117 tabte pladser i stedet for 2n til 3n og nye certifikater for ordenerne 62 til 118. Dermed er alle ordener fra 3 dækket.

Åben forbliver foreløbig den uafhængige kontrol: en genopbygning på en fremmed computer (er allerede udført af forfatteren), helst med lean4checker, og en bedømmelse af fagfolk. Lean-filerne er i denne beskrivelse endnu ikke linket offentligt. Desuden stiller Gukov på sin side et spørgsmål, som beviset ikke besvarer: Hvorfor virker celleværdierne tilfældige, mens de tilhørende potentialfelter ser glatte ud? Yderligere varianter af puslespillet er tænkelige, men der lover intet om dem.

Et puslespil, der begyndte med en bikubefigur med 19 felter, er løst for enhver størrelse. Det krævede først et menneskes idé, så AI som søger og bevisassistent og til sidst en kontrollant, der ikke tror på nogen af de involverede, men efterregner hvert trin.