Как искусственный интеллект покоряет большую математику: от Навье — Стокса до упаковки сфер и Lean

Всем привет! Меня зовут Игорь Росляков, я технический писатель.

В свете недавних сообщений о том, что новейшая разработка OpenAI справилась с одной из величайших математических проблем, мы подготовили аналитический материал и пообщались с директором Института прикладного искусственного интеллекта и цифровых технологий РЭУ им. Г. В. Плеханова, членом‑корреспондентом РАН Александром Храмовым. Мы обсудили интеграцию ИИ в научную среду, принципы перевода сложных концепций на машинный язык и последствия этих открытий для нашего будущего.

Основные темы материала:

• Пионеры универсального символического языка науки

• Как добиться абсолютной технической верификации доказательств

• Lean как специализированная среда разработки для исследователей

• Проблема оптимального плотного размещения сфер

• Текущий статус уравнений Навье — Стокса

• Действительно ли модель справилась с задачей Навье — Стокса

• Суть проблемы и практическая ценность доказательства

• Степень задействования формализации

• Ключевые итоги и выводы

Пионеры универсального символического языка науки

Фундаментальным инструментом современной формальной математики выступает язык Lean.

Однако ему предшествовали труды ряда мыслителей, стремившихся переложить научное знание на рельсы строгой и безальтернативной проверки. Хотя их прямые наработки редко применяются в Lean напрямую, их исторический вклад бесценен. Краткую справку об этих ученых мы спрятали под спойлер.

Готлоб Фреге, Давид Гильберт и Курт Гёдель

Готлоб Фреге (1848–1925) — выдающийся немецкий логик, философ и математик.

В 1879 году он разработал концепцию Begriffsschrift — один из прародителей современных формальных систем логики. Ученый стремился структурировать умозаключения так, чтобы их логика подчинялась железным законам, исключая многозначность естественной речи.

Давид Гильберт (1862–1943) — один из величайших математиков на стыке XIX и XX столетий.

В труде «Основания геометрии» (1899) он представил дисциплину в виде аксиоматического каркаса. Если классический подход опирается на наглядные образы («через две точки проводится прямая»), то Гильберт предложил абстрагироваться: зафиксировать базовые сущности и исчерпывающий перечень аксиом, из которых законным путем выводятся остальные следствия.

Широко известна его мысль о том, что вместо «точек и плоскостей» с тем же успехом можно оперировать «стульями и кружками» — суть кроется не в природе объектов, а в связывающих их правилах. В этом и заключается суть формализации: искусственному интеллекту не требуется интуитивное понимание терминов, ему важны синтаксические правила.

Общая логика выглядит следующим образом:

аксиомы → допустимые правила вывода → теорема

При непрерывном контроле каждого шага доказательство превращается в цепочку валидных переходов. Сам этот процесс перевода научных задач на машинный язык получил название формализации.

В начале 1920-х годов Гильберт инициировал масштабную программу по представлению математики в качестве единой непротиворечивой системы аксиом, подлежащей независимому анализу. Это заложило фундамент современной теории доказательств.

Именно его идеи ближе всего подошли к философии Lean.

Курт Гёдель (1906–1978) — знаменитый австрийский математический логик и философ.

https://www.famousmathematicians.net/kurt-godel/

В 1930-х годах Гёдель занялся развитием идей Гильберта, однако его фундаментальные теоремы о неполноте существенно скорректировали первоначальный оптимизм.

Если сильно упростить суть его открытий, то:

1. Любая достаточно сложная непротиворечивая формальная система содержит истинные суждения, которые невозможно ни подтвердить, ни опровергнуть внутри нее.

2. Подобная система неспособна математически доказать собственную непротиворечивость.

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

Временной промежуток между трудами Гёделя и появлением Lean огромен, и мы опустим его детали.

Вкратце отметим: в 1960–1980-х годах появились Automath, Mizar, а затем HOL, Isabelle и Coq. В 2005 году с помощью Coq была верифицирована теорема о четырех красках, а в 2014 году завершился проект Flyspeck, посвященный гипотезе Кеплера. К последнему мы еще вернемся.

Как добиться абсолютной технической верификации доказательств

Формализация — это метод кодирования знаний в строгом синтаксисе, исключающем двусмысленность толкований. Это применимо к математическим теоремам, алгоритмической логике программ или проектной документации в инженерии.

Рассмотрим простейший пример. Человеку интуитивно понятно утверждение:

Квадрат четного числа также является четным числом.

Однако формальная система требует проговаривать каждый промежуточный шаг. Сначала вводится дефиниция четности:

n четно ⇔ существует целое k, при котором n = 2k.

Затем фиксируется исходное условие:

n = 2k.

Производится операция возведения в квадрат:

n² = (2k)² = 4k² = 2(2k²).

И на основе исходного определения делается искомый вывод:

n² — четное.

Человеческий мозг опускает эти очевидные ступени, тогда как формальный верификатор требует четкого обоснования каждого перехода.

Lean — среда разработки для ученых

Язык Lean представляет собой интерактивный ассистент доказательств, функционирующий на базе теории зависимых типов. Последняя позволяет увязывать тип данных с их конкретным содержанием:

• В стандартном программировании типы абстрактны: «число», «строка», «массив».

• Зависимые типы позволяют задавать жесткие рамки вроде «массив строго из 5 элементов» или «положительное число».

В математике это открывает огромные возможности: утверждение становится типом, а доказательство — экземпляром этого типа. Например, выражение «2 + 2 = 4» эквивалентно определенному типу, а само доказательство выступает значением, подтверждающим его корректность. Ошибки в вычислениях сразу приводят к сбою верификации.

Синтаксически это выглядит так:

theorem two_plus_two : 2 + 2 = 4 := by
  rfl

Конструкция theorem two_plus_two задает имя теоремы, после двоеточия следует доказываемая формула:

2 + 2 = 4

Блок := by открывает тело доказательства. Оператор rfl (рефлексивность) предписывает Lean вычислить обе части выражения и сопоставить их. Поскольку 2 + 2 сводится к 4, проверка сводится к очевидному равенству 4 = 4.

До появления Lean существовали иные верификаторы, а также системы символьных вычислений вроде Mathematica, ориентированные главным образом на преобразование формул, а не на логический контроль. Сегодня крупные языковые модели неплохо владеют Lean, опираясь на открытые базы данных вроде Mathlib.

Использование языков программирования вроде Lean автоматизирует рутину, сводя математику к синтаксическим правилам. С базовыми выкладками современные LLM справляются легко (автоформализация), но перед лицом серьезной науки возникают трудности: необходимо наличие всех вспомогательных определений в библиотеках и идеальное соответствие замыслу авторов.

Представьте масштабы задачи, если вместо арифметики требуется формализовать уравнения Навье — Стокса:

Здесь недостаточно пары строчек. Предварительно необходимо задать аппараты производных, функциональные пространства, критерии «гладкости» решений, энергетические оценки — и пройти через мириады промежуточных логических шагов. Человеку на это требуются годы кропотливого труда.

Прежде чем вернуться к тематике OpenAI и гидродинамики, обратимся к прецедентам успешного применения ИИ в данной сфере.

Задача об упаковке сфер

Это классический пример интеграции искусственного интеллекта в процесс формализации результатов высшей математики.

Интуитивную суть проблемы легко представить на примере монет: при их плотном размещении на плоской поверхности неизбежно остаются пустые зазоры. Возникает вопрос об их максимальной концентрации.

На плоскости оптимальным решением является сотовая структура, где каждую монету окружают шесть соседей: 

В трехмерном пространстве задача трансформируется в укладку идентичных шаров (подобно апельсинам на витрине или пушечным ядрам в арсенале).

Данное предположение известно как гипотеза Кеплера (1611 год). Строгое доказательство ее оптимальности было получено Томасом Хейлсом и Сэмюэлом Фергюсоном лишь в 1998 году с привлечением мощных вычислительных систем.

Из-за колоссального объема машинных расчетов рецензенты не смогли верифицировать работу полностью, что побудило Хейлса запустить проект Flyspeck, завершившийся в 2014 году. Это яркий прецедент, когда формализация потребовалась не ради эксперимента, а из-за невозможности людей проверить громоздкое доказательство вручную.

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

Четырехмерный аналог выглядит следующим образом:

Аналогично строятся формулы для восьми измерений, позволяя беспрепятственно вычислять расстояния и объемы.

Исторически одним из первых исследованием плотной укладки занялся Томас Хэрриот на рубеже XVI и XVII веков. Будучи советником мореплавателя Уолтера Рэли, он решал практическую задачу оптимизации складирования пушечных ядер. В трактате 1591 года он рассчитывал параметры пирамидальных конструкций и обсуждал с Кеплером проблему заполнения пространства одинаковыми телами.

Особый интерес представляют пространства размерности 8 и 24, где существуют уникальные симметричные решетки E₈ и Лича. Решетка задает регулярную, строго упорядоченную сетку точек, центрирующих сферы. Для E₈ плотность упаковки невероятно высока, и долгое время ее превосходство носите гипотетический характер.

До 2016 года идеальная упаковка была строго доказана лишь для 1, 2 и 3 измерений. Прорыв совершила математик Марина Вязовская, доказавшая оптимальность E₈ для 8 измерений, а вскоре совместно с коллегами решившая аналогичную проблему для решетки Лича в 24 измерениях. За эти достижения она была удостоена Филдсовской премии 2022 года.

Впоследствии исследователи решили перевести данное доказательство на язык Lean.

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

Инициатива стартовала в марте 2024 года силами студента Сидхарта Харихарана и самой Марины Вязовской, составившей детальную дорожную карту доказательства для последующего переноса в Lean.

К началу 2026 года была выполнена масштабная подготовительная работа, после чего к делу подключилась компания Math, Inc. со специализированным агентом Gauss. Используя репозиторий и карту, Gauss за пять дней закрыл пробелы в восьмимерном случае, а затем за пару недель справился и с 24-мерным, сгенерировав свыше 200 тысяч строк кода на Lean.

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

Здесь важно зафиксировать важнейший рубеж: искусственный интеллект продемонстрировал способность оперировать математикой высшего уровня, опираясь, однако, на известное человечеству целевое решение и намеченный путь.

Задача об упаковке сфер не была исключением — ранее Lean успешно применялся в таких сложных областях, как перфектоидные пространства и Liquid Tensor Experiment.

Следующим логичным вопросом стало: способен ли ИИ самостоятельно прийти к результату, неизвестному научному сообществу?

Текущий статус уравнений Навье — Стокса

Кратко обрисуем сложившуюся обстановку.

Американский Математический институт Клэя в 2000 году учредил награды по одному миллиону долларов за решение семи проблем тысячелетия из различных областей. На сегодня официально покорена лишь гипотеза Пуанкаре, доказанная Григорием Перельманом (от призовых средств он отказался).

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

На протяжении последнего года над ней работали математик Тристан Бакмастер (Нью-Йоркский университет) и Левент Альпёге (Anthropic), задействовав языковые модели Claude и ChatGPT. К началу сентября в академических кругах поползли слухи о скором прорыве.

По версии OpenAI, после появления этих слухов компания 1 сентября задействовала свою новейшую секретную разработку (превосходящую по мощности GPT-6 Astra) для штурма всех семи нерешенных задач. Уже 8 сентября компания официально отчиталась об успешном решении проблемы Навье — Стокса.

Обнаружив сходство методологии модели OpenAI со своими наработками, Тристан Бакмастер запросил у компании разъяснения. Детали этого диалога разбирались в подробной статье на SE7ENе, если же суммировать позиции сторон, то ситуация выглядит следующим образом.

Бакмастер заявляет, что представители OpenAI предлагали ему выпустить совместный релиз без включения в соавторы Альпёге, представляющего конкурирующую Anthropic. Себастьен Бубек из OpenAI отвергает это обвинение, заявляя, что не требовал исключения Альпёге, хотя и принес извинения за некорректную формулировку в беседе.

В OpenAI утверждают, что ни исследователи, ни агенты компании не имели доступа к неопубликованным материалам Бакмастера и Альпёге, хотя допускают утечку обезличенных данных через пользовательские запросы к сервисам. Сэм Альтман охарактеризовал подходы как «различающиеся». Независимо подтвердить эти утверждения пока не представляется возможным.

Примечательно, что 8 сентября Бакмастер и Альпёге опубликовали препринты о потере гладкости для смежных уравнений (включая трехмерные уравнения Эйлера) с формальными доказательствами в Lean. Их собственный материал по Навье — Стоксу пока ждет публикации.

Действительно ли модель справилась с задачей Навье — Стокса

Окончательного ответа пока нет, хотя экспертные оценки звучат сдержанно-оптимистично.

11 сентября 2026 года представители института Клэя констатировали, что проблема, «судя по всему, получила разрешение», но подчеркнули необходимость соблюдения регламента:

Согласно уставу института, работа должна пройти процедуру публикации в рецензируемом математическом издании высшего уровня. После этого запускается двухлетний мораторий на глубокую проверку международным сообществом. Оценка формируется на основе независимых отзывов, обсуждений на конференциях и публикаций в профильных журналах. Отсчет двухлетнего срока стартует с момента выхода статьи в печати, а не с публикации в блоге. Сама компания OpenAI отказалась от претензий на призовой фонд.

Верификацией займутся ведущие мировые специалисты по дифференциальным уравнениям: им предстоит изучить выкладки, воспроизвести ключевые этапы, выявить потенциальные ошибки и опубликовать рецензии.

Суть проблемы и практическая ценность доказательства

С научно-популярным описанием задачи можно ознакомиться на портале thecode.media.

Если опустить технические детали, суть сводится к следующему.

Назначение уравнений Навье — Стокса: математическое описание динамики сплошных сред (жидкостей и газов). Зная начальные параметры (скорость потоков, давление, вязкость, внешние силы), уравнения позволяют прогнозировать их эволюцию. На их основе проектируются обводы самолетов, гидравлические системы и метеорологические модели.

Концепция гладкости. Решения допускают резкие колебания параметров, однако исключают появление математических разрывов или устремление величин к бесконечности. Это не означает ламинарность течения — турбулентные потоки также могут сохранять математическую гладкость.

Суть проблемы тысячелетия. Требовалось выяснить, гарантируют ли трехмерные уравнения сохранение гладкости во времени. Возможны были два исхода: доказательство того, что любые гладкие начальные условия ведут к гладкому решению во все последующие моменты, либо демонстрация хотя бы одного примера образования сингулярности (бесконечного роста скорости за конечный интервал).

Без погружения в сложные формулы обрисуем выводы предложенного решения.

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

Важная ремарка: привлечение внешней силы не противоречит правилам. Условия института Клэя допускают использование гладких затухающих внешних сил. В OpenAI утверждают, что доказали этот сценарий как для бесконечного пространства, так и для периодических граничных условий.

Таким образом, в случае подтверждения результатов, уравнения Навье — Стокса действительно допускают потерю гладкости при разрешенных исходных данных.

Для инженеров и пилотов ничего не изменится: уравнения продолжат штатно использоваться в аэродинамике и метеорологии.

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

Степень задействования формализации

Любопытно, что современному искусственному интеллекту формализация нужна вовсе не для поиска озарения, а для последующей строгой проверки.

Судя по материалам OpenAI, в процессе поиска решения Lean не использовался как базовый инструмент. Около 10 тысяч агентов оперировали привычным математическим языком: анализировали литературу, генерировали гипотезы, выводили формулы и тестировали код, придя к аналитическому результату примерно за 88 часов.

Лишь после завершения поисков доказательство было переведено на язык Lean для машинной верификации, на что ушло еще около 17 часов силами модели GPT-6 Astra.

Выстраивается четкое разделение труда. Эвристический поиск эффективнее вести на естественном языке математики, а Lean выполняет роль автоматического рецензента, сокращающего годы ручной проверки до считанных часов. Тем не менее, остается нюанс: Lean гарантирует лишь правильность синтаксиса кода, тогда как его соответствие исходным требованиям института Клэя должны подтверждать эксперты-люди.

Ключевые итоги и выводы

Все происходящее указывает на индустриализацию научного поиска: подключение вычислительных мощностей ИИ позволяет решать задачи на порядки быстрее традиционных сроков.

Распространено мнение, что говорить об автономности ИИ преждевременно, поскольку постановку задач, отбор данных и контроль осуществляют люди. Но давайте присмотримся к этой схеме.

Верификация результатов постепенно автоматизируется — именно для этого внедряется Lean. В случае с Навье — Стоксом машинная проверка заняла 17 часов, а работу пула агентов координирует алгоритм, а не человек. Базой данных служит вся накопленная математическая литература.

Остается фактор постановки задачи. Но разве это подрывает самостоятельность? Ученые редко формулируют проблемы в вакууме: задачи тысячелетия заданы институтом Клэя, проблемы на столетие вперед — Гильбертом, а текущие темы определяются грантами и индустрией. Никто не умаляет заслуг Перельмана из-за того, что гипотезу Пуанкаре сформулировал не он.

Формулировка задачи задается внешней средой для любого исследователя. Ключевой вопрос — кто находит путь к ответу. Если заявления OpenAI подтвердятся, то от условий до проверенного доказательства ИИ впервые прошел путь самостоятельно.

Уравнения Навье — Стокса подошли идеально благодаря предельной строгости формулировок. В живой науке сложнее всего трансформировать расплывчатую гипотезу в точную математическую постановку, и здесь роль человека пока незаменима.

Постановка проблемы не является признаком несамостоятельности ИИ, это естественное разделение труда: человек определяет ценность цели, а машина берет на себя трудоемкую часть поиска путей решения. Следующим шагом станет способность ИИ самостоятельно определять актуальные вопросы для исследования.

Для обывателя решение уравнения Навье — Стокса не принесет мгновенных изменений, однако практический эффект подобных технологий огромен. Способность систем ускорять проверку моделей, отсекать тупиковые ветви и находить неохотные прорывы неизбежно отразится на материаловедении, фармакологии и инженерии.

 

Источник