Навье — Стокс, упаковка сфер и 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 — формальная проверка доказательства гипотезы Кеплера об упаковке шаров. К ней мы ещё вернёмся.

Как сделать доказательство точно технически проверяемым

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

Вот пример. Допустим, человек понимает такое утверждение:

Если число чётное, то его квадрат тоже чётный.

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

n чётное ⇔ существует целое k, для которого n = 2k.

Потом взять исходное условие:

n = 2k.

После этого возвести число в квадрат:

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

А затем по определению чётности получить:

n² четное.

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

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

Современный Lean — интерактивный proof assistant (система интерактивного доказательства теорем), основанный на теории зависимых типов. Теория зависимых типов означает способ описывать данные так, чтобы тип зависел от конкретного значения. Посмотрите:

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

• В зависимых типах можно выразить гораздо более точное условие, например: «это список ровно из 5 элементов» или «это число, которое больше нуля».

Для математических доказательств это очень удобно, хотя и не сразу понятно, как именно устроено. В Lean утверждение рассматривается как тип, а доказательство — как объект этого типа. Например, утверждение «2 + 2 = 4» можно представить как особый тип, а доказательство — как значение, которое этому типу соответствует. Если такого корректного значения построить нельзя, значит доказательство не прошло проверку.

Выглядеть это будет так:

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

Здесь theorem two_plus_two объявляет теорему с именем two_plus_two. После двоеточия записано утверждение, которое мы хотим доказать:

2 + 2 = 4

После := by начинается само доказательство. rfl означает reflexivity — Lean вычисляет обе стороны выражения и проверяет, что они сводятся к одному и тому же значению. 2 + 2 вычисляется как 4, поэтому для Lean утверждение в итоге превращается в 4 = 4.

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

Язык программирования Lean ещё сильнее всё упрощает, потому что сводит математику к языку программирования с чёткими правилами. С короткими выкладками современные LLM уже справляются: такой перевод называют автоформализацией. Но для серьёзной математики это по-прежнему тяжёлая работа. Нужно, чтобы в библиотеке уже были все используемые понятия, и чтобы формулировка в Lean точно совпадала с тем, что имели в виду математики..

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

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

К истории про Навье — Стокса и OpenAI мы ещё вернёмся, а пока посмотрим на шаг, когда ИИ смог формализовать задачу. 

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

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

Самый простой вариант этой задачи можно представить с монетами. Если положить одинаковые монеты на стол, между ними неизбежно остаются промежутки. Возникает вопрос: как расположить их так, чтобы они заняли максимально возможную долю поверхности?

В двух измерениях ответ выглядит как соты — каждая монета окружена шестью соседями: 

В трёх измерениях задача превращается в укладку одинаковых шаров — как апельсины на прилавке или пушечные ядра в пирамиде. 

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

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

Шары в четырёх и более измерениях уже не нарисовать, хотя математически не происходит ничего загадочного. Обычный трёхмерный шар радиуса r задается условием

Четырёхмёрный — таким:

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

Одним из первых укладывать шарики по-математически начал Томас Хэрриот в конце XVI века. Он был математическим советником мореплавателя Уолтера Рэли, которого интересовал практический вопрос: как считать и складывать пушечные ядра в штабеля, чтобы уместилось побольше? В рукописи 1591 года Хэрриот рассчитывал пирамидальные укладки пушечных ядер, а позже заинтересовался более общим вопросом — как одинаковые шары заполняют пространство.  Этот вопрос он обсуждал в переписке с Кеплером — так и появилась гипотеза Кеплера.

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

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

А потом проект решили формализовать в Lean.

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

Проект стартовал в марте 2024 года. Его начали студент Сидхарт Харихаран и сама Марина Вязовская. Вязовская подготовила подробную карту доказательства, а участники проекта постепенно переводили определения, леммы и необходимые разделы математики в Lean.

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

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

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

Задача об упаковке сфер не была первой — до этого Lean уже использовали для серьёзных проектов современной математики: например, перфектоидных пространств и Liquid Tensor Experiment.

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

Что с задачей Навье — Стокса

Если кратко, ситуация такая.

В США есть математический институт Клэя. В 2000 году он объявил награду за 7 задач, которые назвал математическими проблемами тысячелетия. Среди них оказались задачи из разных разделов математики, от теории чисел до математической физики. За решение каждой присуждается награда в миллион долларов. Пока официально решена только одна — гипотеза Пуанкаре. Её доказал Григорий Перельман, но от премии отказался.

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

Последний год над этой задачей активно работали двое учёных — математик из Нью-Йоркского университета Тристан Бакмастер и Левент Альпёге из Anthropic. Работу они вели с помощью ИИ-моделей Claude от Anthropic и ChatGPT от OpenAI. В начале сентября начали появляться слухи, что задачу эту двое уже почти решили и вот-вот опубликуют доказательство.

По словам самой OpenAI, после слухов о том, что две задачи тысячелетия вот-вот будут решены, 1 сентября компания запустила свою новую внутреннюю модель (её описывают как «значительно более сильную, чем GPT-6 Astra», публичного доступа к ней нет) сразу на все открытые задачи из списка. А 8 сентября OpenAI опубликовала у себя новость о том, что эта их новая модель решила задачу тысячелетия.

Тристан Бакмастер вроде как понял, что метод модели OpenAI почему-то очень похож на их с Альпёге подход. Понятно, он принялся писать в OpenAI с целью разузнать, как это вышло. На Хабре уже есть отличная подробная статья о том, что получилось из этого разговора, но если коротко, позиции сторон такие.

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

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

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

Решила ли модель Навье — Стокса на самом деле

Пока неизвестно, хотя первые реакции осторожно оптимистичные.

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

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

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

О чём задача и что с этого доказательства нам

Чуть подробнее о задаче простым языком можно прочесть тут: thecode.media. Только учитывайте, что это не техническое, а научно-популярное объяснение.

Если совсем кратко, то смысл такой.

Что делают уравнения Навье — Стокса: описывают движение жидкости или газа. Если известно состояние потока сейчас — например, скорости в разных точках, давление, вязкость и действующие силы, — уравнения задают, как это состояние должно меняться дальше во времени. На их основе ещё до решений Бакмастера и OpenAI рассчитывали и рассчитывают движение воздуха вокруг самолёта, воды в трубе и множество других течений.

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

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

На этом месте становится сложно, но для полноты картины попробуем кратко сказать, что показало решение.

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

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

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

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

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

А была ли формализация

Тут получается интересно, потому что, оказывается, современному ИИ формализация нужна не для поиска решения, а для его проверки.

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

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

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

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

Что из этого можно вынести в качестве выводов

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

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

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

Остаётся постановка задачи. Но разве это аргумент против самостоятельности? Учёные-люди тоже редко придумывают задачи с нуля. Задачи тысячелетия сформулировал институт Клэя, 23 проблемы на век вперёд — Гильберт в 1900 году, а большинство исследователей работают над вопросами, которые ставят научные руководители, гранты и индустрия. Никто не скажет, что Перельман доказал гипотезу Пуанкаре «несамостоятельно», потому что не сам её придумал.

Задачу для ИИ всегда кто-то ставит — так же, как её ставят для любого исследователя. Важно другое: кто находит путь к ответу. И если описание OpenAI подтвердится, то путь от формулировки до проверенного доказательства ИИ впервые прошёл практически сам.

Интересно, что Навье — Стокс подошёл для этого идеально: задача сформулирована предельно строго, и понятно, что считать ответом. А самая трудная часть живой науки часто в другом — превратить размытый вопрос «почему так происходит?» в точную постановку. Вот здесь роль человека пока действительно ключевая. 

Постановка задачи — не признак несамостоятельности ИИ, а нормальное разделение труда в науке. Человек определяет, что важно и зачем это нужно, а ИИ всё лучше отвечает на вопрос «как». Следующий рубеж — не решить поставленную задачу, а научиться видеть, какие вопросы вообще стоит задавать.

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