Magiczny sześciokąt: znaleziony z AI dla każdego rozmiaru

Zagadka z plastrami miodu ma teraz odpowiedź dla każdego rozmiaru. Dowód znalazł autor przy pomocy AI, a asystent dowodzenia Lean sprawdził go maszynowo; niezależna recenzja jeszcze trwa. Tutaj wyjaśniamy go bez żargonu.

Magiczny sześciokąt to łamigłówka liczbowa rozgrywana na polach przypominających plaster miodu. Dowód, że takie sześciokąty istnieją w każdym rozmiarze, znaleziono przy pomocy AI i sprawdzono maszynowo w Lean. Zautomatyzowane poszukiwanie dowodu zajęło kilka godzin czasu obliczeniowego. Chodzi tu wyłącznie o zagadkę matematyczną, a nie o pojęcie o tej samej nazwie z polityki gospodarczej.

Artykuł najpierw wyjaśnia, czego wymaga zagadka, i śledzi drogę od pierwszego sześciokąta do dowodu. Następnie przedstawia ideę dowodu w pięciu elementach, każdy z ilustracją. Na końcu omawia, dlaczego można ufać dowodowi sprawdzonemu przez komputer, co mimo to musi sprawdzić człowiek oraz jakie liczby i fakty kryją się za wynikiem.

Magiczny sześciokąt: czego wymaga łamigłówka liczbowa

Pole gry to figura z plastrów miodu w kształcie foremnego sześciokąta. Jego rozmiar nazywa się rzędem n i mówi, ile pól leży na jednym boku. Sześciokąt rzędu n składa się z 3n(n−1)+1 pól. Dla n = 3 to 19 pól, dla n = 10 już 271.

W pola wpisuje się liczby całkowite tak, aby każdy prosty rząd dawał tę samą sumę. Liczy się rzędy we wszystkich trzech kierunkach figury. W każdym kierunku jest 2n−1 rzędów. Najkrótsze przy brzegu mają n pól, środkowy ma 2n−1 pól.

Najsłynniejszy magiczny sześciokąt zawiera liczby od 1 do 19 i ma rząd 3. Każdy rząd daje 38. To klasyczny sześciokąt i dla liczb zaczynających się od 1 istnieje tylko ten jeden rozmiar, w którym zagadka się domyka. Proste rozważanie o podzielności pokazuje, że wymagana suma rzędu jest liczbą całkowitą tylko dla n = 1 i n = 3. Dla wszystkich innych rzędów klasyczny wariant zawodzi więc już na starcie.

Dlatego nowa praca dotyczy pokrewnego wariantu. Zamiast zaczynać od 1, używa się liczb całkowitych od −K do K, każdej dokładnie raz. Przy tym K = 3n(n−1)/2. Dla n = 3 są to liczby od −9 do 9, dla n = 10 liczby od −135 do 135. Każdy rząd daje 0, a pośrodku stoi 0.

Zagadka brzmi niewinnie, ale jest trudna. Liczba możliwych wypełnień rośnie z n tak szybko, że zwykłe próbowanie na komputerze daleko nie zaprowadzi. Potrzebny był więc plan konstrukcji działający dla każdego rozmiaru oraz dowód, że ten plan naprawdę zawsze się udaje.

Od zagadki z 1887 roku do największego znanego sześciokąta: droga do dowodu

Pierwotny problem pochodzi od Ernsta von Haselberga i zwykle datuje się go na rok 1887. Niektóre źródła podają 1888, ale źródła pierwotnego nie przejrzano. Później Adams, według własnej relacji, ponownie odkrył klasyczny sześciokąt w 1957 roku i upowszechnił go dzięki rubryce Martina Gardnera. Że to rozwiązanie jest, z dokładnością do obrotu i odbicia, jedyne, udowodnił Charles W. Trigg, publikacja z 1964 roku. Zbiór materiałów prowadzi Uniwersytet w Bielefeld, przegląd oferuje Wolfram MathWorld.

Wariant z kolejnymi liczbami całkowitymi i sumą 0 pojawił się później. W latach 2004 do 2006 znaleziono rzędy od 4 do 8: rząd 6 w październiku 2004, rzędy 7 i 8 w 2006 roku. Do 2006 roku największym znanym rozwiązaniem był tylko rząd 8. Mniejsze rzędy były już wtedy rozwiązane. Przegląd z odnośnikami do źródeł daje niemieckojęzyczna Wikipedia, której daty bywają podane bez źródła.

W 2024 roku Dr. DSGVO, autor tego bloga, znalazł przy pomocy AI rozwiązanie rzędu 9. Było to wówczas największe znane rozwiązanie.

2 sierpnia 2026 roku Konstantin Gukov opublikował na swojej stronie New magic hexagons pewien wzorzec. Szukał rozwiązań do rzędu 21 i zauważył, że można z nich prawdopodobnie wyprowadzić przepis konstrukcyjny dla dowolnie dużych sześciokątów. Gukov opisał do tego algorytm i szkic dowodu, który miał działać dopiero od rzędu 114. Sam zaznacza, że ten szkic nie jest sformalizowany w Lean ani niezależnie sprawdzony. Dowód wciąż więc nie istniał.

Dla tej luki istnieje teraz dowód dla wszystkich rzędów od 3. Powstał przy pomocy AI i jest udokumentowany w opisie z 21 października 2026 roku. Lean sprawdził go maszynowo, niezależna recenzja jeszcze trwa, a pliki Lean nie są jeszcze publicznie podlinkowane. Więcej o tym dalej.

Magiczne sześciokąty dla wszystkich rozmiarów: co jest udowodnione

Udowodnione jest: dla każdego rzędu n od 3 istnieje magiczny sześciokąt z liczbami od −K do K, w którym każdy rząd we wszystkich trzech kierunkach ma sumę 0. Udowodniona jest też wersja zaostrzona, w której dodatkowo pośrodku stoi 0. Nie ma przy tym górnej granicy. Szkic Gukova działa dopiero od rzędu 114, wcześniejsze rzędy pozostawały bez ostatniego elementu otwarte.

Pokrycie jest stopniowane. Rząd 2 jest niemożliwy, ponieważ siedmiu liczb od −3 do 3 nie da się odpowiednio rozmieścić. Ta część nie należy do dowodu w Lean. Dla rzędów od 3 do 6 istnieją gotowe sześciokąty, które Lean sprawdził liczba po liczbie. Dla rzędów od 7 do 61 działa ogólny plan konstrukcji, uzupełniony o jedno sprawdzone rozwiązanie podzagadki. Dla rzędów od 62 do 118 jest tak samo, tyle że potrzebne listy obliczono na nowo i sprawdzono. Od rzędu 119 wystarcza stały plan konstrukcji, ogólnie udowodniony dla każdego n.

Dwa twierdzenia główne podsumowują całość. Pierwsze mówi, że dla każdego n od 3 istnieje magiczny sześciokąt rzędu n. Drugie mówi to samo dla wersji zaostrzonej z zerem pośrodku. Oba twierdzenia nie mają założeń poza n ≥ 3.

Dowód w pięciu elementach: przegląd

Dowód można sobie wyobrazić jako drabinę. Każdy element zmniejsza zadanie, aż na końcu zostaje tylko kolejność siedzeń na ławce. Elementy od 1 do 4 były już sprawdzone. Nowy jest piąty element, czyli kolejność siedzeń dla każdego rozmiaru. To on domyka dowód.

Kolejne sekcje omawiają elementy po kolei. Pierwsze trzy są poglądowe, ostatnie dwa mogą być nieco bardziej techniczne. Wszystkie rachunki sprawdził Lean, więc w tekście wystarczą idee.

Element 1: wystarczy jedna szósta, bo naprzeciwko stoi liczba przeciwna

Nie trzeba planować całego sześciokąta, wystarczy jedna szósta. Każde pole ma pole przeciwległe, położone symetrycznie względem środka. Jeśli w jednym polu stoi liczba a, w polu przeciwległym stanie −a. W ten sposób każda liczba jest zużyta razem ze swoją przeciwną, a 0 zostaje dla środka.

Ma to praktyczną konsekwencję dla rzędów. Rząd odbity ma dokładnie przeciwną sumę. Jeśli jeden rząd jest wyrównany, jego odbicie też. Rzędy przez środek są wręcz wyrównane same z siebie.

Sześciokąt rozpada się wokół środka na sześć jednakowych trójkątów. Trzy z nich to trójkąty pól przeciwległych: ich liczby wynikają z odbicia przez środek z odwróconym znakiem. Dwa kolejne to kopie szóstego trójkąta obrócone o 120 stopni i dostają ściśle powiązane liczby. Zostaje jeden wolny trójkąt z T = n(n−1)/2 polami. Dla n = 10 to 45 zamiast 271 pól.

Warunek „każdy rząd ma sumę 0” zamienia się w ten sposób w warunek dla tego trójkąta. Dla każdego rzędu ważona suma jego wpisów musi dać zero. Tę sumę nazywamy dalej bilansem rzędu.

Element 2: każda liczba staje się bazą plus cyfrą

W drugim kroku każdą liczbę rozkłada się na dwie części: bazę i cyfrę. Obie części wyrównuje się osobno. Ponieważ sumy rzędów przy dodawaniu po prostu się dodają, sześciokąt jest magiczny, gdy obie części są wyrównane każda z osobna.

Zasób liczb od 1 do 3T dzieli się w tym celu na trójki: k, T+k i 2T+k dla k od 1 do T. Każda trójka to baza T+k plus T razy cyfra, przy czym cyfra to −1, 0 lub 1. W sześciokącie rzędu 3 mamy T = 3, a zasób sięga od 1 do 9. Baza 4 daje 1, 4 i 7, baza 5 daje 2, 5 i 8, baza 6 daje 3, 6 i 9.

Zadanie rozpada się więc na dwie niezależne zagadki. Pierwsza to pole cyfr złożone z −1, 0 i 1 z bilansem zero w każdym rzędzie. Druga to pole baz, w którym wartości od T+1 do 2T rozmieszcza się i opatruje znakami tak, aby bilans każdego rzędu wynosił zero.

Element 3: pole cyfr rośnie jak drabina

Pole cyfr jest w pełni rozwiązane dla każdego rzędu od n = 5, i to przez indukcję w krokach co trzy. Zasadę zna każda drabina: kto ma pierwszy szczebel i regułę przejścia do następnego, dosięgnie każdego szczebla.

Najpierw są gotowe, wyrównane pola cyfr dla promieni 4, 5 i 6. Promień to tu n−1. Potem obowiązuje reguła dobudowy: wyrównane pole cyfr można rozszerzyć o trzy nowe warstwy na brzegu. Nowe warstwy mają taki wzór, że w każdym rzędzie wzajemnie się znoszą. Od 4 idzie się tak do 7, 10, 13 i dalej, od 5 do 8, 11 i dalej, od 6 do 9, 12 i dalej. W ten sposób osiąga się każdy promień od 4.

Ta część prawie nie kosztuje czasu obliczeń przy sprawdzaniu. Rozwiązuje jednak tylko pierwszą z dwóch podzagadek, pole baz pozostaje otwarte.

Element 4: pożądane odstępy, które wzajemnie się równoważą

Pola baz nie szuka się bezpośrednio. Zamiast tego najpierw dla każdej pary pól ustala się, o ile mają się różnić jej dwie bazy. Te pożądane odstępy są ogólnie udowodnione dla wszystkich rzędów od n = 13.

Prawie wszystkie pola trójkąta tworzą pary leżące symetrycznie względem jego osi środkowej. Jedno pole pary dostaje minus, drugie plus. W bilansie zostaje wtedy tylko różnica obu wartości, wspólny udział T odpada. Liczy się więc tylko odstęp obu rang. Ranga to po prostu numer miejsca: baza T+k ma rangę k.

Pożądane odstępy powstają w kilku krokach. Są koła łączności: małe wzory z czterech par pól z wagami +1 i −1 i bilansem zero w każdym rzędzie. Nazwa pochodzi od reguły rachunkowej, że w sumach można przestawiać nawiasy bez zmiany wyniku. Każda suma takich wzorów także ma bilans zero. Z wielu wzorów powstaje pole główne, w którym żadna para pól nie dostaje odstępu 0. Odstęp 0 byłby bezużyteczny, bo dwa pola nigdy nie mogą nosić tej samej liczby.

Pola na osi środkowej nie mają partnera. Dostają one najmniejsze rangi 1, 2, 3 i tak dalej, a pole główne dokładnie równoważy ich wkład. Pola przekątnej niosą dodatkowo udział T, który się nie znosi. Równoważą go dwa rozgałęzione łańcuchy par pól, zwane lasami. Ich odstępy powiększa się o około T/2, razem więc o T.

Wynikiem jest pełny zestaw pożądanych odstępów z bilansem zero w każdym rzędzie, z których żaden nie wynosi zero. Większość odstępów jest mała i wynosi najwyżej 12. Pola pierwszego wiersza mają odstępy do około 2n, pary z lasów odstępy bliskie T/2.

Element 5: kolejność siedzeń dla każdego rozmiaru

Na koniec rangi od 1 do T trzeba faktycznie rozmieścić tak, aby każda para pól dostała dokładnie swój pożądany odstęp. Od n = 119 dzieje się to według stałego planu konstrukcji, a poniżej tej wartości za pomocą list znalezionych przez komputer i sprawdzonych przez Lean.

Można to sobie wyobrazić jako kolejność siedzeń na długiej ławce z T miejscami. Pola przekątnej siedzą na stałe na pierwszych miejscach 1, 2, 3 i tak dalej. Każda para pól potrzebuje dwóch miejsc w przepisanym odstępie. Żadne miejsce nie może być zajęte dwukrotnie. Dokładnie n−1 miejsc pozostaje wolnych. Przypadają one polom brzegowym bez partnera, dla których każde miejsce jest dobre.

Decydującą sztuczką są bloki. Pary o tym samym odstępie g można układać bez luk. Dla g = 3 pary (1, 4), (2, 5) i (3, 6) wypełniają miejsca od 1 do 6 bez luki. Ogólnie g par z odstępem g wypełnia dokładnie 2g kolejnych miejsc, po czym następuje kolejny blok. Dzięki temu każda grupa odstępów marnuje co najwyżej g−1 miejsc na końcu swojego ostatniego bloku. Grupy z odstępami od 1 do 12 kosztują razem co najwyżej 0+1+…+11 = 66 miejsc.

Ławkę dzieli się od przodu do tyłu na pięć stref. W pierwszej strefie siedzi przekątna. Potem następuje okno gwiazdy, w którym specjalny rząd par jest zagnieżdżony jak tęcze jedna w drugiej, a w luki pasują pary z odstępami 6 i 8. W oknie lasu siedzą pary o bardzo dużych odstępach, ich partnerzy lądują daleko z tyłu w zarezerwowanym obszarze. Potem idą klasy reszt, czyli wszystkie pozostałe pary z odstępami od 1 do 12 w blokach. Na końcu n−1 pól brzegowych zajmuje miejsca, które zostały.

Dlaczego plan konstrukcji działa dopiero od n = 119? Ławka jest zapełniona prawie co do miejsca. Wolne mogą zostać tylko tyle miejsc, ile jest pól brzegowych bez partnera, czyli n−1. Plan traci co najwyżej 117 miejsc: 18 w oknie gwiazdy, 66 w blokach, 21 w oknie lasu i 12 przy przeskakiwaniu. Udaje się więc, gdy tylko n−1 wynosi co najmniej 118. Dla n = 119 wolnych jest 118 miejsc, a traci się najwyżej 117, zostaje więc jedno miejsce zapasu.

Dla mniejszych rozmiarów program komputerowy szukał pasujących kolejności siedzeń i zapisał je jako listy liczb. Te listy nazywają się certyfikatami. Lean sprawdza każdy certyfikat samodzielnie, zamiast ufać programowi szukającemu.

Dlaczego można ufać dowodowi: Lean sprawdza każdy krok

Dowód nie tylko został spisany, lecz sprawdzony wiersz po wierszu przez program weryfikujący. Lean to język programowania do dowodów matematycznych. Każdy wniosek zapisuje się tak dokładnie, że komputer może go przeliczyć. Nie ma tam luk ani „oczywiście”. Błąd przerwałby kompilację.

Wykorzystuje się przy tym Mathlib, wielką wspólną bibliotekę już sprawdzonej matematyki dla Lean, na przykład reguł rachunkowych dla zbiorów skończonych i sum. W gotowym dowodzie nie ma ani jednego „sorry”. Tak w Lean nazywa się zastępnik, którym można tymczasowo pominąć krok. Nie ma też własnego aksjomatu (nieudowodnionego założenia podstawowego) ani zaufania do skompilowanego kodu programu. Lean potrafi na końcu wypisać, na jakich założeniach opiera się twierdzenie. Tutaj są to tylko trzy zwyczajowe, na których opiera się praktycznie cała Mathlib: propext, Classical.choice i Quot.sound.

Programy w Pythonie, które znalazły certyfikaty i plan konstrukcji, nie muszą być wolne od błędów. Błędny certyfikat lub błędny plan zostałby odrzucony przez Lean. To właściwy zysk z użycia AI i programów szukających: narzędzia mogą zgadywać, a sprawdzanie i tak jest ścisłe.

Co musi sprawdzić człowiek: definicja w pięciu wierszach

Jedno ograniczenie dotyczy każdego dowodu sprawdzonego przez komputer: definicji na początku się nie sprawdza, tylko zakłada. W tym przypadku definicja ma zaledwie pięć wierszy i mówi w języku potocznym tak: istnieje wypełnienie pól liczbami całkowitymi. Żadne dwa pola nie noszą tej samej wartości. Użyte wartości to dokładnie liczby od −K do K. Każdy rząd w każdym z trzech kierunków ma sumę 0. W wersji zaostrzonej pośrodku stoi dodatkowo 0.

Trzy możliwe furtki są wykluczone. Po pierwsze, pola i liczby do siebie pasują: sześciokąt ma 3n(n−1)+1 pól i dokładnie tyle samo jest liczb od −K do K, więc „każda liczba dokładnie raz” jest wymuszone. Po drugie, wartości poza plastrem się nie liczą, wszystkie warunki dotyczą tylko pól w sześciokącie. Po trzecie, rzędy poza plastrem są puste, ich suma wynosi automatycznie 0, co jest nieszkodliwe. Wzór na K używa dzielenia całkowitego, co jest bezpieczne, bo n(n−1) jest zawsze parzyste.

Podczas sprawdzania zauważono też lukę, która została już zamknięta. Pierwotna definicja nie wymagała wprost zera pośrodku. Konstrukcja co prawda zawsze je daje, ponieważ pola przeciwległe noszą wartości przeciwne. Mimo to istnieje teraz zaostrzona definicja z dodatkowym warunkiem, że środek wynosi 0, a drugie twierdzenie główne dowodzi jej dla wszystkich n od 3.

Pozostaje resztkowe zaufanie, jak przy każdym dowodzie formalnym. Dotyczy ono małego jądra weryfikującego Lean i podstawowych definicji Mathlib, na przykład sum i przedziałów. Użyto wersji wstępnej Lean 4. Ponadto sprawdzanie przebiegło dotąd w jednym środowisku. Bezpieczniej będzie, gdy ktoś niezależnie skompiluje pliki na własnym komputerze. Opcjonalnie osobny program kontrolny, taki jak lean4checker, może jeszcze raz sprawdzić gotowe pliki dowodu. Dla małych rozmiarów można ponadto wypisać konkretny sześciokąt i przeliczyć go ręcznie. Niczego to dodatkowo nie dowodzi, ale poglądowo pokazuje, że definicja oddaje to, co zamierzono.

Liczby i fakty o dowodzie

O twierdzeniu: udowodniony jest magiczny sześciokąt z sumą zero dla każdego rzędu n od 3, także z zerem pośrodku. Gotowe sześciokąty istnieją dla n od 3 do 6. Dla n od 7 do 118 certyfikaty dają rozwiązanie zagadki baz, z czego 57 jest nowych, mianowicie te dla n od 62 do 118. Ogólny plan konstrukcji obowiązuje od n = 119, co odpowiada promieniowi 118. Traci on najwyżej 117 miejsc i zostawia przy n = 119 co najmniej jedno miejsce zapasu. Największy rząd certyfikatu to n = 118, co odpowiada 6 903 polom w trójkącie.

O rozmiarze: elementy od 1 do 4 oraz certyfikaty do n = 61 zebrano w jednym pliku liczącym 2 713 wierszy. Element 5 składa się z 40 plików i około 7 000 wierszy. Największe zapotrzebowanie na pamięć wynosi 5,9 gigabajta, i to przy pliku dotyczącym pierwszego wiersza planu konstrukcji. Użyto Lean 4 w wersji wstępnej v4.35.0-rc4 oraz Mathlib. Jako aksjomaty pojawiają się tylko propext, Classical.choice i Quot.sound, otwartych luk nie ma.

O czasie obliczeń: ponowna kompilacja elementu 5 trwa około 38 minut, certyfikaty równolegle potrzebują około 23 minut. Pojedyncze pliki trwają wyraźnie dłużej. Plik z elementami od 1 do 4 potrzebuje 460 sekund, plik pomocniczy ze wzorami pożądanych odstępów 897 sekund, certyfikaty dla n od 62 do 89 kolejnych 437 sekund, a te dla n od 90 do 117 kolejnych 927 sekund. Pliki dotyczące pierwszego wiersza potrzebują razem około 18 minut. Te czasy opisują ponowną kompilację gotowego sprawdzenia. Całe zautomatyzowane poszukiwanie dowodu wraz z wyszukiwaniem i rozwojem kosztowało kilka godzin.

O testach wstępnych: plan konstrukcji przetestowano numerycznie przed dowodem w Lean, jako dokładne odwzorowanie definicji dla promieni od 118 do 450. Twierdzenia pomocnicze sprawdzono do promienia 20 000. Te testy były tylko wstępną kontrolą, sam dowód to tekst w Lean.

Co dalej: otwarte pytania i ocena

Praca Gukova i dowód w Lean się uzupełniają. Gukov dostarczył wzorzec, konstrukcję i szkic z granicą 114. Szkic nie przeliczał luk pierwszego wiersza i lasów. Ustawione naiwnie, brakowałoby tam łącznie około 2n do 3n miejsc, więcej niż dozwolone n−1. Dowód w Lean zaczyna się właśnie w tym miejscu. Dostarcza wzorów na pożądane odstępy, planu upakowania z co najwyżej 117 utraconymi miejscami zamiast 2n do 3n oraz nowych certyfikatów dla rzędów od 62 do 118. W ten sposób pokryte są wszystkie rzędy od 3.

Otwarta pozostaje na razie niezależna kontrola: ponowna kompilacja na obcym komputerze (autor już ją przeprowadził), możliwie z lean4checker, oraz recenzja specjalistów. Pliki Lean nie są w tym opisie jeszcze publicznie podlinkowane. Gukov stawia ponadto na swojej stronie pytanie, na które dowód nie odpowiada: dlaczego wartości pól wyglądają na losowe, podczas gdy odpowiadające im pola potencjałów wyglądają gładko? Możliwe są dalsze warianty zagadki, ale nic się w tej sprawie nie obiecuje.

Zagadka, która zaczęła się od figury z 19 pól, jest rozwiązana dla każdego rozmiaru. Potrzebny był do tego najpierw pomysł człowieka, potem AI jako poszukiwacz i asystent dowodzenia, a na końcu weryfikator, który nie wierzy nikomu z uczestników, tylko przelicza każdy krok.