Магічний шестикутник: знайдено за допомогою ШІ для будь-якого розміру

Головоломка про магічний шестикутник із бджолиних стільників тепер має відповідь для кожного розміру. Автор знайшов доказ за допомогою ШІ, а асистент доведення Lean перевірив його машинно; незалежна рецензія ще попереду. Тут доказ пояснено без фахової мови.

Магічний шестикутник — це числова головоломка, у якій грають на стільникових клітинках. Доказ того, що такі шестикутники існують у кожному розмірі, знайшли за допомогою ШІ та машинно перевірили в Lean. Автоматизований пошук доказу забрав кілька годин обчислювального часу. Тут ідеться саме про математичну головоломку, а не про однойменне поняття з економічної політики.

Стаття спочатку пояснює, чого вимагає головоломка, і простежує шлях від першого шестикутника до доказу. Далі йде ідея доказу в п'яти будівельних блоках, кожен із малюнком. Наприкінці розглянуто питання, чому можна довіряти доказу, перевіреному комп'ютером, що все одно має перевірити людина та які цифри й факти стоять за результатом.

Магічний шестикутник: чого вимагає числова головоломка

Ігрове поле — стільникова фігура у формі правильного шестикутника. Її розмір називається порядком n і показує, скільки клітинок лежить на одній стороні. Шестикутник порядку n складається з 3n(n−1)+1 клітинок. Для n = 3 це 19 клітинок, для n = 10 уже 271.

У клітинки записують цілі числа так, щоб кожен прямий ряд мав однакову суму. Ряди рахують в усіх трьох напрямках стільникової фігури. У кожному напрямку є 2n−1 рядів. Найкоротші на краю мають n клітинок, середній має 2n−1 клітинок.

Найвідоміший магічний шестикутник містить числа від 1 до 19 і має порядок 3. Кожен ряд дає в сумі 38. Це класичний шестикутник, і для чисел, що починаються з 1, це єдиний розмір, у якому головоломка розв'язується. Просте міркування про подільність показує, що потрібна сума ряду є цілим числом лише при n = 1 і n = 3. Тож для всіх інших порядків класичний варіант не спрацьовує вже на старті.

Тому нова робота обертається навколо спорідненого варіанта. Замість того щоб починати з 1, беруть цілі числа від −K до K, кожне рівно один раз. Тут K = 3n(n−1)/2. Для n = 3 це числа від −9 до 9, для n = 10 — числа від −135 до 135. Кожен ряд дає в сумі 0, а в центрі стоїть 0.

Головоломка звучить невинно, але вона складна. Кількість можливих заповнень зростає з n так швидко, що перебір на комп'ютері далеко не заведе. Тому потрібен був кресленик, який працює для будь-якого розміру, і доказ того, що цей кресленик справді завжди спрацьовує.

Від головоломки 1887 року до найбільшого відомого шестикутника: історія

Первісна задача походить від Ернста фон Хазельберга, і її зазвичай датують 1887 роком. Деякі джерела називають 1888 рік; першоджерело не переглядали. Пізніше, за його власними словами, Адамс заново відкрив класичний шестикутник у 1957 році та зробив його відомим через колонку Мартіна Гарднера. Те, що це розв'язання єдине з точністю до повороту й віддзеркалення, довів Чарльз В. Тригг, публікація 1964 року. Збірку матеріалів на цю тему веде Білефельдський університет, а огляд пропонує Wolfram MathWorld.

Варіант із послідовними цілими числами та сумою 0 потрапив у поле зору пізніше. Між 2004 і 2006 роками знайшли порядки від 4 до 8: порядок 6 — у жовтні 2004 року, порядки 7 і 8 — у 2006 році. До 2006 року як найбільше розв'язання був відомий лише порядок 8. Менші порядки на той час уже були розв'язані. Огляд із посиланнями на джерела подає німецька Вікіпедія, дати в якій подекуди без підтвердження.

У 2024 році доктор DSGVO, автор цього блогу, знайшов за допомогою ШІ розв'язання порядку 9. Тоді це було найбільше відоме розв'язання.

2 серпня 2026 року Костянтин Гуков опублікував на своїй сторінці New magic hexagons закономірність. Він шукав розв'язання до порядку 21 і помітив, що з них, імовірно, можна вивести правило побудови для як завгодно великих шестикутників. Гуков описав алгоритм і начерк доказу, який мав діяти, починаючи з порядку 114. Він сам зазначає, що цей начерк не формалізований у Lean і не перевірений незалежно. Отже, доказу ще бракувало.

Для цієї прогалини тепер є доказ для всіх порядків від 3. Його створено за допомогою ШІ, і він задокументований в описі від 21 жовтня 2026 року. Lean перевірив його машинно, незалежна рецензія ще попереду, а файли Lean поки що публічно не опубліковані. Про це далі.

Магічні шестикутники для всіх розмірів: що доведено

Доведено: для кожного порядку n від 3 існує магічний шестикутник із числами від −K до K, у якому кожен ряд в усіх трьох напрямках має суму 0. Доведено й посилену версію, у якій додатково 0 стоїть у центрі. Верхньої межі немає. Начерк Гукова діє лише від порядку 114; порядки до нього без останнього блока залишалися відкритими.

Охоплення поетапне. Порядок 2 неможливий, бо сім чисел від −3 до 3 не вдається розподілити належним чином. Ця частина не входить до доказу в Lean. Для порядків від 3 до 6 є готові шестикутники, які Lean перевірив число за числом. Для порядків від 7 до 61 діє загальний кресленик, доповнений однією перевіреною відповіддю до допоміжної головоломки. Для порядків від 62 до 118 так само, лише необхідні списки було перераховано й перевірено. Від порядку 119 достатньо фіксованого кресленика, загально доведеного для кожного n.

Дві головні теореми підсумовують це. Перша стверджує, що для кожного n від 3 існує магічний шестикутник порядку n. Друга говорить те саме про посилену версію з 0 у центрі. Обидві теореми не мають жодної умови, крім n ≥ 3.

Доказ у п'яти блоках: огляд

Доказ можна уявити як драбину. Кожен блок зменшує завдання, доки не лишиться тільки план розсаджування на лаві. Блоки з 1 по 4 уже були наявні в перевіреному вигляді. Новий — п'ятий блок, план розсаджування для кожного розміру. Він завершує доказ.

Наступні розділи розглядають блоки по черзі. Перші три наочні, останні два можуть бути дещо технічнішими. Усі обчислення перевірив Lean, тож у тексті досить самих ідей.

Блок 1: досить однієї шостої, бо навпроти стоїть протилежне число

Планувати весь шестикутник не потрібно, достатньо однієї шостої. Кожна клітинка має протилежну клітинку, що лежить дзеркально відносно центру. Якщо в одній клітинці стоїть число a, у протилежну йде −a. Так кожне число вичерпується разом зі своїм протилежним, а 0 лишається для центру.

Це має практичний наслідок для рядів. Дзеркальний ряд має рівно протилежну суму. Якщо один ряд збалансований, то й його дзеркальне відображення теж. Ряди через центр збалансовані самі собою.

Шестикутник навколо центру розпадається на шість однакових трикутників. Три з них — трикутники протилежних клітинок: їхні числа випливають із віддзеркалення через центр із протилежним знаком. Ще два — копії шостого трикутника, повернуті на 120 градусів, і отримують тісно пов'язані числа. Лишається єдиний вільний трикутник із T = n(n−1)/2 клітинок. Для n = 10 це 45 замість 271 клітинки.

Умова «кожен ряд має суму 0» тим самим стає умовою на цей трикутник. Для кожного ряду зважена сума його елементів має дорівнювати нулю. Цю суму далі називаємо балансом ряду.

Блок 2: кожне число стає базою плюс цифрою

На другому кроці кожне число розкладають на дві частини: базу й цифру. Обидві частини балансують окремо. Оскільки суми рядів при додаванні чисел просто додаються, шестикутник стає магічним, щойно обидві частини збалансовані самі по собі.

Для цього запас чисел від 1 до 3T ділять на групи по три: k, T+k і 2T+k для k від 1 до T. Кожна група — це база T+k плюс T, помножене на цифру, де цифра дорівнює −1, 0 або 1. Для шестикутника порядку 3 маємо T = 3, і запас іде від 1 до 9. База 4 дає 1, 4 і 7, база 5 дає 2, 5 і 8, база 6 дає 3, 6 і 9.

Отже, завдання розпадається на дві незалежні головоломки. Перша — поле цифр із −1, 0 і 1 з нульовим балансом у кожному ряду. Друга — поле баз, у якому величини від T+1 до 2T розподіляють і наділяють знаками так, щоб баланс кожного ряду був нульовим.

Блок 3: поле цифр росте, як драбина

Поле цифр повністю розв'язане для кожного порядку від n = 5 за допомогою індукції кроками по три. Принцип знайомий кожному з драбиною: хто має перший щабель і правило переходу до наступного, досягне будь-якого щабля.

Спочатку є готові збалансовані поля цифр для радіусів 4, 5 і 6. Радіус дорівнює n−1. Потім діє правило добудови: збалансоване поле цифр можна розширити трьома новими шарами на краю. Нові шари мають такий візерунок, що в кожному ряду взаємно знищуються. Від 4 так доходимо до 7, 10, 13 і далі, від 5 до 8, 11 і далі, від 6 до 9, 12 і далі. Так досягається кожен радіус від 4.

Ця частина при перевірці майже не потребує обчислювального часу. Проте вона розв'язує лише першу з двох допоміжних головоломок; поле баз лишається відкритим.

Блок 4: бажані відстані, що взаємно врівноважуються

Поле баз шукають не безпосередньо. Натомість спершу для кожної пари клітинок визначають, на скільки мають відрізнятися їхні дві бази. Ці бажані відстані загально доведені для всіх порядків від n = 13.

Майже всі клітинки трикутника утворюють пари, що лежать дзеркально відносно його осі симетрії. Одна клітинка пари отримує мінус, інша — плюс. У балансі лишається тільки різниця двох величин; спільна частина T випадає. Отже, важлива лише відстань між двома рангами. Ранг — це просто номер місця: база T+k має ранг k.

Бажані відстані виникають у кілька кроків. Є кола асоціативності: невеликі візерунки з чотирьох пар клітинок із вагами +1 і −1 та нульовим балансом у кожному ряду. Назва походить від арифметичного правила, за яким у сумах дужки можна переставляти без зміни результату. Кожна сума таких візерунків також має нульовий баланс. Із багатьох візерунків утворюється головне поле, у якому жодна пара клітинок не отримує відстань 0. Відстань 0 була б непридатною, бо дві клітинки ніколи не можуть мати те саме число.

Клітинки на осі симетрії не мають партнера. Вони отримують найменші ранги 1, 2, 3 і так далі, а головне поле точно врівноважує їхній внесок. Діагональні клітинки додатково несуть частку T, яка не скорочується. Її врівноважують два розгалужені ланцюги пар клітинок — ліси. Їхні відстані збільшують приблизно на T/2, разом отже на T.

Результат — повний набір бажаних відстаней з нульовим балансом у кожному ряду, жодна з яких не дорівнює нулю. Більшість відстаней малі й не перевищують 12. Клітинки першого рядка мають відстані до приблизно 2n, пари лісів — відстані, близькі до T/2.

Блок 5: план розсаджування для кожного розміру

Нарешті ранги від 1 до T справді треба розподілити так, щоб кожна пара клітинок отримала рівно свою бажану відстань. Від n = 119 це робить фіксований кресленик; нижче — списки, знайдені комп'ютером і перевірені Lean.

Це можна уявити як план розсаджування на довгій лаві з T місцями. Діагональні клітинки сидять на фіксованих місцях — перших 1, 2, 3 і так далі. Кожна пара клітинок потребує двох місць на приписаній відстані. Жодне місце не може бути зайняте двічі. Рівно n−1 місць лишається вільним. Їх отримують крайові клітинки без партнера, яким підходить будь-яке місце.

Вирішальний прийом — блоки. Пари з однаковою відстанню g можна складати без проміжків. Для g = 3 пари (1, 4), (2, 5) і (3, 6) заповнюють місця з 1 по 6 без проміжку. Загалом g пар із відстанню g заповнюють рівно 2g послідовних місць, потім іде наступний блок. Так кожна група відстаней марнує щонайбільше g−1 місць наприкінці свого останнього блока. Групи з відстанями від 1 до 12 разом коштують щонайбільше 0+1+…+11 = 66 місць.

Лаву поділено спереду назад на п'ять зон. У першій зоні сидить діагональ. Далі йде зоряне вікно, у якому особливий ряд пар вкладається одна в одну, як веселки, а в проміжки вміщаються пари з відстанями 6 і 8. У віконці лісу сидять пари з дуже великими відстанями, чиї партнери опиняються далеко позаду в зарезервованій ділянці. Після цього йдуть класи лишків, тобто усі інші пари із відстанями від 1 до 12 блоками. Нарешті n−1 крайових клітинок займають місця, що лишилися.

Чому кресленик діє лише від n = 119? Лава майже точно заповнена. Вільними можуть лишитися тільки стільки місць, скільки є крайових клітинок без партнера, тобто n−1. Кресленик втрачає щонайбільше 117 місць: 18 у зоряному вікні, 66 у блоках, 21 у віконці лісу та 12 при пропусканні. Тож усе виходить, щойно n−1 не менше 118. Для n = 119 вільних 118 місць, а втрачено щонайбільше 117, отже лишається одне місце запасу.

Для менших розмірів комп'ютерна програма шукала відповідні плани розсаджування й зберігала їх як числові списки. Ці списки називаються сертифікатами. Lean сам перевіряє кожен сертифікат, а не довіряє пошуковій програмі.

Чому доказу можна довіряти: Lean перевіряє кожен крок

Доказ не лише записаний, а й перевірений рядок за рядком програмою перевірки доведень. Lean — це мова програмування для математичних доведень. Кожен висновок записується так точно, що комп'ютер може його перерахувати. Прогалин або слова «очевидно» там немає. Помилка призвела б до переривання трансляції.

Використовується Mathlib — велика спільна бібліотека вже перевіреної математики для Lean, наприклад для правил арифметики зі скінченними множинами та сумами. У готовому доказі немає жодного «sorry». Так у Lean називається заглушка, якою крок можна тимчасово пропустити. Немає й власної аксіоми (недоведеного основного припущення) та довіри до перекладеного програмного коду. Наприкінці Lean може перелічити, на яких основних припущеннях тримається теорема. Тут це лише три звичайні, на яких побудована практично вся Mathlib: propext, Classical.choice і Quot.sound.

Програми на Python, які знайшли сертифікати й кресленик, не мусять бути безпомилковими. Хибний сертифікат або хибний кресленик Lean відхилив би. У цьому справжня користь від ШІ та пошукових програм: інструменти можуть здогадуватися, а перевірка все одно сувора.

Що має перевірити людина: означення в п'яти рядках

Одне обмеження діє для кожного доведення, перевіреного комп'ютером: означення на початку не перевіряється, а приймається. У цьому випадку означення має лише п'ять рядків, і повсякденною мовою воно каже таке: існує заповнення клітинок цілими числами. Жодні дві клітинки не мають однакового значення. Використані значення — рівно числа від −K до K. Кожен ряд у кожному з трьох напрямків має суму 0. У посиленій версії додатково 0 стоїть у центрі.

Три можливі лазівки виключено. По-перше, клітинки та числа збігаються: шестикутник має 3n(n−1)+1 клітинок, і від −K до K є рівно стільки ж чисел, тож «кожне число рівно один раз» забезпечується примусово. По-друге, значення поза шестикутником не враховуються; усі умови стосуються лише клітинок усередині шестикутника. По-третє, ряди поза шестикутником порожні, їхня сума автоматично 0, що безпечно. Формула для K використовує цілочисельне ділення, що не викликає сумнівів, бо n(n−1) завжди парне.

Перевірка виявила також прогалину, яку відтоді усунено. Початкове означення прямо не вимагало 0 у центрі. Побудова її завжди дає, бо дзеркальні клітинки мають протилежні значення. Попри це тепер є посилене означення з додатковою умовою, що центр дорівнює 0, і друга головна теорема доводить його для всіх n від 3.

Певна залишкова довіра лишається, як і в кожному формальному доведенні. Вона стосується невеликого ядра перевірки Lean і базових означень Mathlib, наприклад для сум та інтервалів. Використовували попередню версію Lean 4. Крім того, перевірка досі виконувалася в єдиному середовищі. Надійніше буде, коли хтось незалежно скомпілює файли на власному комп'ютері. За бажання окрема програма контролю, як-от lean4checker, може ще раз перевірити готові файли доказу. Для малих розмірів також можна вивести конкретний шестикутник і перерахувати його вручну. Це нічого додатково не доводить, але наочно показує, що означення передає те, що мається на увазі.

Цифри та факти про доказ

Щодо твердження: доведено магічний шестикутник із нульовою сумою для кожного порядку n від 3, також із 0 у центрі. Готові шестикутники існують для n від 3 до 6. Для n від 7 до 118 сертифікати дають розв'язання базової головоломки, з яких 57 нових, а саме для n від 62 до 118. Загальний кресленик діє від n = 119, що відповідає радіусу 118. Він втрачає щонайбільше 117 місць і при n = 119 лишає щонайменше одне місце запасу. Найбільший порядок сертифіката — n = 118, що відповідає 6 903 клітинкам у трикутнику.

Щодо обсягу: блоки з 1 по 4 і сертифікати до n = 61 зведено в один файл на 2 713 рядків. Блок 5 складається з 40 файлів приблизно по 7 000 рядків загалом. Найбільша потреба в пам'яті становить 5,9 гігабайта, для файла про перший рядок кресленика. Використовували Lean 4 у попередній версії v4.35.0-rc4 і Mathlib. Як аксіоми з'являються лише propext, Classical.choice і Quot.sound, відкритих прогалин немає.

Щодо обчислювального часу: перебудова блока 5 триває близько 38 хвилин, сертифікати паралельно потребують близько 23 хвилин. Окремі файли потребують значно більше. Файл із блоками з 1 по 4 потребує 460 секунд, допоміжний файл із формулами бажаних відстаней — 897 секунд, сертифікати для n від 62 до 89 — ще 437 секунд, а для n від 90 до 117 — ще 927 секунд. Файли про перший рядок разом потребують близько 18 хвилин. Ці часи описують перебудову готової перевірки. Увесь автоматизований пошук доказу з пошуком і розробкою забрав кілька годин.

Щодо попередніх тестів: перед доказом у Lean кресленик числово перевіряли як точну копію означень для радіусів від 118 до 450. Допоміжні твердження перевіряли до радіуса 20 000. Ці тести були лише попередньою перевіркою; сам доказ — це текст Lean.

Що далі: відкриті питання та контекст

Робота Гукова й доказ у Lean доповнюють одне одного. Гуков дав закономірність, побудову та начерк із межею 114. Начерк не перераховував прогалини першого рядка й лісів. Якби їх закласти наївно, там разом бракувало б приблизно від 2n до 3n місць, більше за дозволені n−1. Доказ у Lean починається саме з цього місця. Він дає формули для бажаних відстаней, план пакування щонайбільше з 117 втраченими місцями замість від 2n до 3n і нові сертифікати для порядків від 62 до 118. Так охоплено всі порядки від 3.

Поки що відкритою лишається незалежна перевірка: перебудова на стороннім комп'ютері (її вже виконав автор), бажано з lean4checker, і рецензія фахівців. Файли Lean в цьому описі ще не опубліковані. Крім того, Гуков на своїй сторінці ставить питання, на яке доказ не відповідає: чому значення клітинок виглядають випадковими, тоді як відповідні потенціальні поля здаються гладкими? Інші варіанти головоломки можливі, але нічого не обіцяється.

Головоломку, що почалася зі стільникової фігури з 19 клітинок, розв'язано для кожного розміру. Для цього спершу була потрібна ідея людини, потім ШІ як шукач і асистент доведення, а насамкінець перевіряльник, який не вірить нікому з учасників, а перераховує кожен крок.