Пчелиные соты, 24 измерения и нейросеть. Как ИИ проверил главную математическую работу десятилетия

Когда украинский математик Марина Вязовская получила Филдсовскую медаль летом 2022 года, научное сообщество восприняло событие как историческое. Вязовская стала лишь второй женщиной за 86 лет существования премии. Спустя почти четыре года имя исследовательницы снова оказалось в центре внимания. На этот раз повод связан не с новым доказательством, а с неожиданным союзом математики и искусственного интеллекта: компьютерные системы сумели формально проверить её сложнейшие доказательства.

Речь идёт о знаменитой задаче упаковки сфер. Математики давно пытаются понять, насколько плотно одинаковые шары можно разместить в пространстве. В двумерном мире лучший вариант напоминает пчелиные соты, в трёхмерном — пирамиду из шаров. Дальше задача становится почти неразрешимой. С ростом числа измерений поиск оптимальной конфигурации превращается в одну из самых сложных проблем современной математики.

В 2016 году Вязовская совершила прорыв. Исследовательница доказала, что в восьмимерном пространстве наилучшую упаковку образует симметричная структура, известная как решётка E8. Чуть позже совместно с коллегами математик показала, что в 24 измерениях оптимальную плотность даёт так называемая решётка Лича. На первый взгляд результат кажется чисто абстрактным, однако подобные конструкции лежат в основе кодов коррекции ошибок — технологий, которые используют смартфоны, спутники и космические аппараты для передачи данных без потерь.

Математическое сообщество тщательно проверило доказательства и признало работу безупречной, что и принесло Вязовской Филдсовскую медаль. Но существует ещё один уровень проверки — формальная верификация. В таком подходе компьютер пошагово проверяет каждое логическое утверждение доказательства. Перевести огромный математический текст в форму, понятную машине, крайне трудно, поэтому многие известные доказательства до сих пор не прошли подобную процедуру.

Интерес к формализации неожиданно возродился после случайной встречи в Лозанне. Там Вязовская познакомилась со студентом Сидхарт ХариХаран, который изучал формальную запись доказательств и использовал её как способ глубже понять математические идеи. Разговор привёл к запуску проекта Formalising Sphere Packing in Lean. Участники начали переводить доказательство упаковки сфер в язык Lean — специальной системы, позволяющей компьютеру проверять математические рассуждения на абсолютную корректность.

Команда сначала подготовила подробную «карту» доказательства, где перечислила все ключевые шаги и указала, какие части уже формализованы, а какие требуют дополнительной работы. Репозиторий проекта постепенно рос, и к середине 2025 года разработчики открыли публичный доступ к материалам.

Затем к истории подключился стартап Math, Inc., который разрабатывает систему искусственного интеллекта под названием Gauss. Модель сочетает языковую обработку текста с формальными математическими инструментами. Алгоритм умеет искать научные статьи, вызывать внешние инструменты, писать код для Lean и сразу запускать проверку доказательства.

Компания уже привлекала внимание научного мира. Ранее система Gauss сумела формализовать сильную форму теоремы о распределении простых чисел — задачей занимались лауреат Филдсовской медали Теренс Тао и математик Алекс Конторович. Искусственный интеллект справился за несколько недель.

Когда разработчики Gauss подключились к проекту упаковки сфер, система быстро доказала десятки промежуточных утверждений и даже обнаружила опечатку в материалах проекта. Затем наступила пауза, но инженеры продолжали улучшать модель. Новая версия алгоритма оказалась значительно мощнее. В январе 2026 года Gauss снова запустили на задаче формализации доказательства Вязовской.

Компьютеру понадобилось всего пять дней, чтобы полностью формализовать доказательство для восьмимерного пространства. Алгоритм снова обнаружил ошибку в опубликованной работе и автоматически её исправил. Но самый впечатляющий результат появился чуть позже: Gauss сумел формализовать и доказательство для 24 измерений. Объём проекта превышал 200 тысяч строк кода, а система справилась всего за две недели.

Для математиков событие выглядит переломным моментом. Формальная проверка доказательств долго считалась чрезвычайно трудоёмким процессом, требующим огромного количества ручной работы. Теперь часть нагрузки берёт на себя искусственный интеллект.

Разработчики подчёркивают, что успех стал результатом совместной работы людей и машин. Математики создали теорию, подготовили структуру доказательства и построили основу проекта, а алгоритм помог быстро заполнить недостающие элементы и проверить логическую целостность всей конструкции.

По мнению создателей Gauss, подобные инструменты могут изменить саму практику математических исследований. Компьютеры возьмут на себя рутинную проверку и техническую формализацию, а исследователи сосредоточатся на главном — поиске новых идей и открытии неизвестных математических миров.