GPT-5.6 Sol помогла доказать: магические шестиугольники существуют для любого порядка n>3

Магический шестиугольник, аналог магического квадрата на шестиугольной сетке: числа в нём образуют прямые линии в трёх направлениях, и сумма чисел на каждой линии одинакова. «Нормальным» шестиугольник называют, если в нём стоят подряд идущие числа от 1 и до общего числа ячеек. Оказывается, единственный нетривиальный нормальный магический шестиугольник в природе, всего один, и в нём ровно 19 ячеек; для всех прочих порядков n>3 сумма чисел просто не делится на число линий, так что нормальных решений там не существует. Это и стало поводом для истории: вопрос всплыл в разговоре выпускников школы ШАД, когда ей исполнилось 19 лет, и кто-то заметил, что 19, ещё и число ячеек этого единственного шестиугольника.

Чтобы не заканчивать на этом, автор обратился к «ненормальным» магическим шестиугольникам, там числа тоже идут подряд, но не обязательно начинаются с 1. Такие решения не выводятся формулой, их ищут только полным перебором по огромному пространству вариантов; по данным Википедии на июль 2026 года, рекордным был шестиугольник порядка n=9, найденный Клаусом Меффертом в 2024 году.

Автор сузил пространство поиска: он рассмотрел антисимметричные шестиугольники (числа от −K до K, где противоположные по центру ячейки дают в сумме ноль) и показал, что любой такой шестиугольник раскладывается по базису «колец» из шести ячеек с чередующимися +1/−1, это уже гарантирует нулевую сумму на каждой линии, оставляя лишь требование различности и последовательности чисел. С этой идеей он обратился не к универсальным решателям вроде Z3 или OR-Tools, а к модели GPT-5.6 Sol, по его словам, языковые модели оказались неожиданно сильны именно в разработке узкоспециализированных решателей. Модель связала задачу с массивами Хеффнера и предложила архитектуру решателя на основе имитации отжига; после нескольких раундов оптимизации (Numba для горячих циклов, поиск узких мест через perf) программа стала быстрее ещё на 50%. Запущенная на домашнем сервере примерно на 24 ядрах CPU в течение нескольких дней, она нашла новые магические шестиугольники для всех порядков вплоть до n=21.

Найденные решения навели автора на гипотезу, что такие шестиугольники существуют для любого n>3, и он решил проверить, способен ли ИИ доказать это математически. Он задействовал две системы: GPT-5.6 Sol как основную модель для рассуждений и Aristotle, агента для формальных доказательств на языке Lean. Параллельная работа с Aristotle зашла в тупик; тогда автор ослабил гипотезу до утверждения о бесконечном числе решений, но и это застопорилось. Затем GPT-5.6 Sol в режиме максимальных вычислений («max») потратила много часов и тоже не нашла доказательства, но сгенерировала несколько идей, которые сохранились в общем контексте проекта. В одном из следующих диалогов та же модель в режиме «high» подхватила эти идеи и собрала из них рабочую конструкцию: сначала конструктивное доказательство для всех порядков n>800, кратных 16, затем, после серии обобщений, для порядков, кратных 8, затем 4, затем 2, и наконец без каких-либо ограничений на делимость. Доказанный порог при этом снизился с 800 до 114. Автор подчёркивает, что 114, не фундаментальный предел метода, а лишь удобная граница, ниже которой доказательство труднее обосновать строго, хотя на практике конструкция работает и для меньших порядков. В сочетании с шестиугольниками, найденными перебором до n=21, итоговый результат покрывает все порядки n>3.

Автор оговаривается: на момент публикации доказательство не формализовано на Lean и не прошло независимую проверку, это следующий шаг. Он описывает смену своей роли в проекте: начинал как «второй пилот» при ИИ, а закончил скорее «пассажиром», направляя модель в перспективные стороны, пока основную творческую работу делала она.

Ключевые факты

• Единственный нетривиальный нормальный магический шестиугольник в мире имеет 19 ячеек; для остальных порядков нормальных решений не существует по арифметической причине (сумма чисел не делится на число линий)
• С помощью модели GPT-5.6 Sol автор разработал специализированный решатель на основе имитации отжига и нашёл новые ненормальные магические шестиугольники для всех порядков до n=21, прежний рекорд (Клаус Мефферт, 2024) был n=9
• Модель GPT-5.6 Sol (в режимах high и max) вместе с Lean-агентом Aristotle несколько дней пытались доказать существование таких шестиугольников для любого n>3; попытка с Aristotle зашла в тупик, но одна из сессий с GPT-5.6 Sol собрала рабочее доказательство
• Доказанный порог поэтапно снижался с n>800 (кратных 16) до n>114 без ограничений на делимость; вместе с перебором до n=21 это покрывает все порядки n>3
• Доказательство пока не формализовано на языке Lean и не прошло независимую проверку, это заявлено как следующий шаг работы

Почему это важно

Это конкретный, воспроизводимый пример, где ИИ не просто ускорил рутину, а сдвинул нерешённую математическую задачу: специализированный решатель, написанный и оптимизированный моделью, нашёл новые объекты (магические шестиугольники до n=21), а затем та же модель, ведомая исследователем, собрала конструктивное доказательство существования таких объектов для всех порядков n>3, задачу, которую десятилетиями решали только перебором. История показывает разработку одного и того же инструмента для двух разных типов работы: генерации кода решателя и построения математического доказательства.

Кому это важно

Математикам и любителям комбинаторики, которым интересны магические фигуры и задачи существования; исследователям, изучающим применение больших языковых моделей и агентов формальной верификации (вроде Aristotle) в математике; разработчикам, которые ищут примеры, как LLM справляются с разработкой узкоспециализированных решателей лучше универсальных инструментов вроде Z3 и OR-Tools.

Как это применить

Автор описывает воспроизводимый метод: сузить пространство поиска за счёт симметрии задачи (антисимметрия, разложение по базису «колец»), поручить модели написать и итеративно оптимизировать специализированный решатель (в этом случае, имитацию отжига на Numba), а затем, найдя достаточно примеров, попросить модель обобщить закономерность в доказательство, подключив при необходимости агента формальной проверки. Исходный код решателя и подробности хода работы автор выложил в блоге.

Можно ли доверять

Источник, личный блог автора работы, без независимой публикации или рецензирования; численные результаты (шестиугольники до n=21) получены прямым компьютерным перебором и проверяемы напрямую, а вот доказательство для n>114 на момент публикации не формализовано на Lean и не прошло независимую проверку, сам автор прямо об этом пишет и называет это следующим шагом.

Риски и подводные камни

Главный риск, именно неформализованность доказательства: агент Aristotle, специально предназначенный для формальной проверки на Lean, параллельную попытку так и не довёл до результата, а итоговое доказательство от GPT-5.6 Sol пока проверено только «вручную» автором и вычислительно, без формальной верификации. Порог n>114 назван удобной, а не фундаментальной границей метода, что оставляет пространство для уточнений и возможных ошибок в промежуточной зоне между переборными и доказанными порядками.

«Мой главный вывод, что языковые модели могут быть на удивление эффективны в разработке узкоспециализированных решателей, оставляя далеко позади такие универсальные инструменты, как Z3 и OR-Tools.»

— автор блога