Еще немного про тектоническое и апокалиптичное сейчас в мире математики. New Scientist сегодня пишет, что OpenAI “неправильно перевела математику в код” в своем доказательстве для уравнений Навье–Стокса. Ну то есть доказательство на “машинной” математике не бьется с доказательством на “человеческой”. Отсюда будто бы следует, что и решение задачи тысячелетия провалилось. Мы поговорили с парой математиков кто хоть немного следит за этой историей и понимает, что происходит, и почитали, что пишут сами причастные. Так вот говорят, что не так все просто (а когда оно бывает так?!). Но главное, для математики история серьезнее, чем сама по себе драма вокруг Навье–Стокса. Напомним, о чем вообще речь. 8 сентября OpenAI объявила, что её внутренняя модель доказала, мол, решения трёхмерных уравнений Навье–Стокса могут “взорваться” за конечное время (математический такой термин, решение уравнения перестаёт существовать как гладкая функция, потому что какая-то величина за конечное время уходит в бесконечность). OpenAI тогда заявляет, что закрыла этим пункт C (и заодно D) официальной формулировки задачи. Около 10 000 агентов дошли до результата за 88 часов, а ещё 17 часов ушло на перевод в Lean с помощью GPT-6 Astra. На выходе получилось два артефакта: PDF на 166 страниц для людей и код на Lean для компьютера. А Lean — это язык, в котором каждый ход логический проверяет машина, он для этого и создавался. Если код компилируется без проблем, значит, утверждение, записанное в Lean, доказано. Поэтому Lean-версию доказательства многие восприняли да и сейчас считают автоматическим подтверждением корректности. Любопытно, что Институт Клэя, который задачи тысячелетия и курирует, при этом результат не принял и обещает оценить его подчёркнуто неторопливо и максимально строго, вручную. По правилам решение должно выйти в научном журнале и продержаться на глазах у математического сообщества минимум два года, тогда его можно засчитывать (по крайней мере, сами математики должны признать). И вот 6 октября Андерс Хансен и Фабиан Чирчелли из Кембриджа вместе с Александром Бастунисом из Королевского колледжа Лондона выложили препринт с вызывающим по меркам математики названием “Навье–Стокс: трудности перевода: Почему проверка в Lean того, что ИИ автоформализовал, не гарантирует верности исходного доказательства на естественном языке”. Они пишут, что Lean-код — это ни разу не перевод PDF. Это вообще другое доказательство, а местами и доказательство другого утверждения (!!!). У OpenAI сначала статью с доказательством написала одна модель, человеческим языком, как это публикуется у математиков друг для друга (на 166 стр, по которым потом живой математик идет и сам считает и проверяет). А потом другая модель перевела эту “человеческую” версию в Lean для отдельной, машинной проверки. Вот эту “машинную” версию они и называют автоформализацией. Ну и повторимся, многие считают, что если Lean-код проверен машиной, без сбоев отработал, а именно это происходит, значит, статья прошла проверку и с ней порядок, а в этом случае — значит, решена задача тысячелетия с уравнениями Навье-Стокса. Так вот авторы говорят, не сходятся две версии и очень сильно. Например, лемма 8.6. В “человеческой” версии доказательства сказано (не пугайтесь только): чтобы оценить m производных решения, хватит m+4 производных исходной функции. В Lean доказано то же самое, но при условии m+5. Конечно, если робот сумеет приготовить омлет из пяти яиц, а в рецепте говорится, что надо из четырех, то он будет в целом прав. Да только мы все равно не можем ручаться, что получится из четырех. Если с омлетом это не так, может быть, критично, а с уравнениями — категорически. Дальше — больше. В другом месте не отдельные значения отличаются у “машинной” и “человеческой” версий, а целый цепочка математической логики. Например, в 10.19, пишут авторы разбора, внутри леммы о единственности решения. “Человеческая” версия опирается на классическую оценку преобразований Рисса в пространстве L^{3/2} со ссылкой на учебник Стейна. А “машинная” на Lean обходит её через вложение Соболева и L² и получает другую оценку, с величиной, которой в “человеческой” версии вообще нет. Лучше это или хуже — не так уж и важно, важно, что это другое. Это что, творческий подход в математике появляется у нейронок, как для “своих”, для машин, так начинает отбиваться от рук и свое что-то проталкивать? Авторы разбора пишут, что вторая модель, которая переводила доказательство в Lean, судя по всему, пыталась просто сделать все, чтобы код скомпилировался, то есть “машинная” версия таки сработала. А это, как вы понимаете, две разные задачи — решить задачу тысячелетия или чтобы тебе конфетку дали, что ты молодец (получить работающий год, а значит, выполнить задачу пользователя: сделать работающий код, и не так уж важно какой и для чего). Так что если что-то из “человеческой” версии никак не ложится в формальный код на Lean, то тем хуже для “человеческой” версии доказательства. Раз такое дело, автор не иронично дали ChatGPT заведомо неверное доказательство с ошибкой в кратности корней многочлена и попросили перевести его в Lean. Модель молча нашла правильные корни и выдала корректный код. Ошибки человека как будто и не было, никакого упоминания. Как они пишут, это закон Гудхарта в чистом виде: когда мера становится целью, она перестает быть хорошей мерой. Код скомпилировался? Скомпилировался. На что жалуешься, человече? Один из авторов говорит, что модель пытается помочь, но именно этим и не помогает. С другой стороны, а какая разница, если теорема верна? Результат же есть? Кевин Баззард из Имперского колледжа, один из главных людей в мире Lean, напоминает, что формулировка теоремы и её доказательство — вообще-то, разные вещи. Если формулировка записана в Lean правильно, а доказательство компилируется, значит, теорема доказана. Так что Навье–Стокс решен. А вот у доказательства в “человеческой” версии могут быть проблемы — там надо ждать пока люди разберутся, для них же писалось. Источники: - препринт Bastounis, Circelli, Hansen — arxiv.org/abs/2610.08144 - обзор в New Scientist @sci_one_tv