История началась с вопроса, чем интересно число 19. В разговоре выпускников YSDA, когда школе исполнилось 19, кто-то заметил: 19 — простое число-близнец, а ещё это число клеток единственного нетривиального нормального магического шестиугольника.
Магический шестиугольник — это сетка, где все прямые линии из клеток в трёх направлениях дают одну и ту же сумму. Нормальный вариант содержит последовательные числа от 1 до 3n²-3n+1. Для n>3 его не существует: сумма всех чисел не делится на число линий 2n-1. Так что единственный нетривиальный нормальный вариант — порядок 3, и в нём ровно 19 клеток.
Дальше автор пошёл в сторону аномальных магических шестиугольников: числа по-прежнему идут подряд, но не обязаны начинаться с 1. До этого самое большое известное решение n=9 нашёл Клаус Мефферт в 2024 году. Формул не было, только перебор огромного пространства.
Автор добавил ограничение antisymmetry: в центре 0, а противоположные клетки содержат противоположные значения. Тогда каждая линия автоматически даёт сумму 0. Ещё он выяснил, что любой zero-sum шестиугольник раскладывается на локальные кольца из шести клеток — «поле потенциалов» порядка n-1. Это помогло уменьшить пространство поиска.
Вместо общих решателей вроде Z3 и OR-Tools автор отдал задачу GPT-5.6 Sol. До этого, готовя задачи для Midnight Code Cup 2026, он успел заметить, что LLM хорошо справляются именно со специализированными решателями. GPT-5.6 Sol связала задачу с Heffter arrays и написала кастомный симулированный отжиг. Автор добавил Numba, оптимизировал узкие места с perf и запустил программу на домашнем сервере с 24 ядрами. Так нашлись аномальные магические шестиугольники всех порядков до n=21.
Возникла гипотеза: такие шестиугольники существуют для любого n>3. Сначала GPT-5.6 Sol (high) и агент Aristotle застряли. GPT-5.6 Sol (max) тоже не доказал утверждение, но выдал несколько свежих идей. Позже эти идеи сработали: получилось конструктивное доказательство для больших n, кратных 16. Его обобщили, порог упал до 114, а потом условие делимости убрали. Конструкция лежит в репозитории gukoff/magic-hexagons и строит шестиугольники любого порядка больше 3. Правда, формальной проверки в Lean пока нет.
Автор замечает: GPT-5.6 Sol отлично копает вглубь, но может зациклиться, поэтому нужен внешний контролёр. Для серьёзной работы он бы запустил несколько моделей с общим контекстом и поиском через exa.ai. Как и в разработке: после появления LLM проверка кода стала узким местом, поэтому важны статические типы и тесты. Математике нужно то же самое — машинная верификация через Lean. Осталось формализовать доказательство, и Aristotle с leanprover/comparator есть чем заняться.