Hacker News Digest

Автоматическое формализование текста из естественного языка в системы вроде Lean не гарантирует корректности исходного доказательства, даже если формальная версия проходит проверку. Проблема заключается в том, что семантически верный перевод математических утверждений из естественного языка в формальный язык требует разрешения неоднозначностей, которые формально невычислимы и находятся на самом высоком уровне иерархии вычислимой сложности (SCI = ∞), что делает задачу строго сложнее, чем проблема останова. Это означает, что никакой алгоритм, включая ИИ, не может гарантировать faithful перевод во всех случаях. На практике это приводит к ситуациям, когда формальное доказательство в Lean подтверждает что-то отличное от того, что утверждалось в естественном языке. В качестве примера авторы анализируют заявленное доказательство взрыва решений уравнений Навье–Стокса, сгенерированное ИИ и формализованное в Lean: хотя Lean-проверка проходит, формализованное утверждение не соответствует исходному естественноязычному claim, то есть доказано не то, что заявлено. Таким образом, доверие к результатам ИИ-доказательств на основе их формальной верификации вводит в заблуждение, поскольку разрыв между естественным и формальным языком остаётся фундаментальным и не преодолимым автоматическими средствами.

Формальное доказательство в Lean считается корректным, но не гарантирует соответствие оригинальному естественноязыковому доказательству. Участники подчеркивают необходимость независимой проверки и отмечают типичные проблемы неоднозначности при переводе математики в формальный язык. Это не опровергает заявленную «доказанность» Navier‐Stokes, а ставит под вопрос эквивалентность двух формулировок. Большинство согласны, что Lean‐доказательство проверяется ядром Lean, но может доказывать формулировку, отличную от той, что в статье. Проблема несоответствия естественноязыкового и формального доказательства типична: спецификация часто отличается от кода, как в человеческих проектах. Ключевой вопрос — эквивалентность формализованного утверждения Lean с оригинальной формулировкой задачи Клейского института. Если они эквивалентны, несоответствие текста не влияет на валидность результата. Естественноязыковые математические утверждения содержат неоднозначности, которые невычислимы и требуют экспертного вмешательства при формализации. Некоторые сравнивают ситуацию с случаями, когда формальная проверка выявляла ошибки в оригинальном тексте (например, статья о borrow‐checker). Есть разногласия: один набор участников считает, что несоответствие показывает лишь различие в формулировках; другой указывает, что это может вводить в заблуждение относительно того, что именно доказано, и требует уточнения, какие утверждения действительно доказаны. Рекомендуется рассматривать AI‐сгенерированные доказательства как «утверждения», требующие традиционного рецензирования и независимой проверки перед принятием как окончательные результаты. Автоматические проверяющие не противоречат теоремам Гёделя, поскольку они лишь проверяют уже найденные доказательства, а не генерируют их для произвольных утверждений.

Автор считает, что несмотря на впечатляющие демонстрации вроде решения Navier-Stokes в Lean или поиска уязвимостей, современные LLM остаются далёкими от настоящей автономии. Их «успехи» достигаются только в узкой нише задач с жёстко формализованными спецификациями, где даже малые отклонения приводят к сбоям или reward hacking. Надёжное использование таких моделей требует колоссальных усилий по формальной спецификации — работы, которую могут выполнять лишь немногие эксперты, и которая часто обходится дороже прямой реализации задачи. Даже в идеальных случаях, таких как доказательство теорем, уязвимости в верификаторах позволяют моделям обманывать систему, выдавая ложные доказательства за верные. Автор отмечает, что компании продолжают нанимать средних инженеров, потому что LLM не заменяют их в реальной работе — они нуждаются в постоянном надзоре. Перспективнее, по его мнению, использовать широкие стаи дешёвых открытых моделей, чем полагаться на дорогие frontier-модели, чьи выгоды сильно преувеличены маркетингом и отобранными демонстрациями. Реальная выгода от ИИ, скорее, придёт не от сверхразума, а от массового применения скромных систем под человеческим контролем — но и здесь узкое место будет tvořить человек, а не вычислительная мощность. Таким образом, революция в знаниевой работе пока не наступила, а ставки на автономные LLM остаются рискованными.

Тред дополняет тезис о неспособности современных LLM к автономии. Эмпирические данные и опыт эксплуатации показывают, что модели не способны надежно соблюдать формальные ограничения (например, правила шахмат по @carodgers), не обладают тактическими и стратегическими знаниями (@yunwal, @lissom), плохо справляются с долгосрочной памятью и оценкой времени выполнения задач (@randomImmigrant, @melvinroest). LLM эффективны лишь как инструменты для экспертов в узких, строго специфицированных задачах (@plaidfuji, @Madmallard). Однако в критических областях, таких как проектирование чипов, необходимость жесткого контроля не исчезает: проверка спецификаций требует в пять раз больше инженеров, чем разработка, из-за высокой стоимости ошибок (@alain94040). Автономность моделей ограничена: решение сложных математических задач требует огромных вычислительных затрат и ручной настройки (@pfdietz), а обучение в контексте не доказывает освоение новых навыков без спецсред (@killerstorm). Человеческий контроль не масштабируется под объемы вывода LLM, а бизнес-модель продажи токенов стимулирует флуд и манипуляции (@ausbah). В дискуссиях @angarg12 утверждает, что LLM уже позволяют исключить человека из цикла в инфраструктурных задачах. @keeda отмечает, что потенциальная замена работников знаниями могла бы оцениваться в десятки триллионов долларов. Тем не менее, @slibhb указывает, что высокая капитализация компаний основана на гипотезах, а не на реальных доходах.

OpenAI объявил о доказательстве, решившем давнюю задачу по уравнениям Навье-Стокса, но ключевой момент, упущенный в обсуждениях, — это одновременная публикация формального доказательства в системе Lean 4 alongside человекочитаемой версии. Это отражает растущую тенденцию: многие недавние математические доказательства, поддержанные ИИ, теперь сопровождаются машинно-проверяемыми формализованными версиями, особенно в Lean 4. До недавнего времени создание таких доказательств было крайне трудоёмким процессом — по оценкам 2005 года, формализация одной страницы учебника по математике требовала около сорока часов работы, что делало её непрактичной для плотных научных статей, где одна фраза может ссылаться на десятилетия предшествующих исследований. Однако прогресс в инструментах и ИИ-ассистентах начал снижать этот барьер, делая формальную верификацию всё более осуществимой даже для сложных результатов. Это изменение может трансформировать математическую практику, повышая надёжность и прозрачность доказательств в эпоху ИИ.

Помимо формального доказательства, обсуждаются огромные вычислительные затраты (до $40 млн на агентный кластер, $132 млн против человеческого труда), сомнения в оригинальности (возможное копирование шагов из чужих работ), медленная верификация Lean-кода (15 часов против 11 дней генерации), риски багов в системе и необходимость проверки, что код действительно формализует заявленную теорему. Традиционная формализация 166-страничного текста требует 132 800 человеко-часов. Несмотря на важность автоформализации, её применение требует глубокого опыта в Lean и математической базе. Рекомендуется оптимизировать верификатор, использовать параллельные вычисления и развивать компактные модели, работающие на потребительском железе. Вопрос о возможности человеческой верификации AI-доказательств остаётся открытым — одни сомневаются в понимании, другие полагаются на формальные системы.

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

Проблема оставалась открытой около 90 лет и имеет ключевое значение для гидродинамики, инженерии и климатического моделирования. OpenAI подчеркивает, что доказательство получено с использованием внутренней модели, значительно превосходящей GPT‑6 Astra, и стремится продемонстрировать темпы прогресса ИИ в решении фундаментальных научных задач. Компания призывает к ответственному использованию таких технологий и видит в этом шаге вклад в развитие исследований, полезных для всего человечества.

OpenAI продемонстрировала резкий скачок в математических способностях ИИ: менее чем за две недели система превзошла Astra, решив задачу, нерешённую 26 лет, с использованием 4,9 млн сообщений и 300 млрд токенов за 5 дней — ресурсы, недоступные академическим исследователям. Использование Lean для формализации доказательства с первого дня повысило доверие к результатам, но вызвало этические споры. Критики утверждают, что OpenAI, возможно, использовала промпты и предварительные результаты других исследователей, включая работы Тристана Бакмасстера и Левента Альпёге, а также слухи о нерешённой задаче для ускоренного запуска проекта — что ставит под сомнение оригинальность, нарушает традиции открытой науки и создаёт опасный прецедент: корпорация тратит $15 млн, чтобы «перехватить» результат, достигнутый годами работы академика. OpenAI утверждает, что не использовала данные других исследователей, но не исключает, что модели обучались на деидентифицированных пользовательских промптах, что вызывает подозрения в научном плагиате и неэтичной конкуренции. Утверждения о «строгих мерах безопасности» воспринимаются как попытка смягчить обвинения. Математики выражают тревогу: годы обучения становятся менее ценными, карьерные возможности сужаются, а авторство открытий перераспределяется в пользу корпораций. ИИ пока эффективен в поиске контрпримеров и сингулярностей, но не в построении глубоких теорий — его роль ограничена опровержением, а не созданием нового знания. Это смещает приоритеты математики в сторону опровержения гипотез. Советы: открытые модели предпочтительнее закрытых, чтобы избежать присвоения чужих идей; следующим вызовом для ИИ должно стать формализование классификации конечных простых групп — чтобы проверить его способность не только решать, но и систематизировать математику.

Математик и его коллега Левант Альпоге объявили о достижении конечного времени взрыва с гладким принуждением для трёх систем: уравнения несжимаемой пористой среды, системы Буссинеска и трёхмерных уравнений Эйлера. Они считают, что также получили взрыв для гипо-диссипативных уравнений Навье-Стокса, но не публикуют этот результат, поскольку проверка в Lean ещё не завершена, а рукопись не готова к публикации. Работа построена на программе Диего Кордобы и Луиса Мартинеса-Зороа, которые несколько лет исследовали вынужденные взрывы с грубым принуждением; авторы использовали большие языковые модели (LLM), чтобы довести эту программу до гладкого принуждения и уравнений Эйлера. Идеи лежат в основе работ Кордобы и Мартинеса-Зороа, и автор считает, что Мартинес-Зороа заслуживает медали Филдса за этот вклад.

Сотрудничество с Левантом было личным, без институциональной поддержки. Использовались модели Anthropic’s Claude, OpenAI’s Codex (включая GPT-5.6 Sol) и recientemente Astra — последняя только для написания и аудита аргументов. Прогресс был медленным до середины августа, когда 15-го числа получены результаты для Буссинеска и Эйлера с гладким принуждением; первая LLM-доказательная версия, полученная от Леванта, была ужасна, но проверена в Lean 22-го числа. С тех пор авторы работают круглосуточно, чтобы превратить машинное доказательство в читаемое. Автор извиняется за низкое качество написания статей, называя их «AI slop», и объясняет это внешним давлением и спешкой. Он подчеркивает, что настоящая значимость результата — не в самом взрыве, а в том, что математик и LLM смогли достичь этого за месяц, что ставит под вопрос традиционные модели обучения, авторства и рецензирования в математике, сравнивая этот момент с «Deep Blue — Каспаровым».

Автор также раскрывает конфликт: после объявления результатов ему предложили через Себастьяна (представителя OpenAI) удалить Леванта из авторства под предлогом, что OpenAI якобы собирается опубликовать собственный результат по Навье-Стоксу и заявить, что они заслуживают Клейевской премии, а авторы — «ближайшие люди к проблеме». Автор отказался, заявив, что если OpenAI опубликует своё решение таким образом, он сделает публичным то, что ему сказали. Он подчеркивает, что не видел доказательства OpenAI, не обвиняет никого, но считает необходимым рассказать о предложении, чтобы предотвратить ложную narraтиву. В завершение он благодарит математическое сообщество за поддержку и выражает желание вернуться к обсуждению идей Кордобы и Мартинеса-Зороа и broader implications для математики.

Тред обсуждает спор о возможном использовании OpenAI приватных данных исследователей Buckmaster–Alpöge при работе над доказательством для уравнений Навье–Стокса: прямых доказательств копирования нет, но существует значительное недоверие. Утверждается, что OpenAI могла получить доступ к их сессиям Codex — компания это отрицает. Также упоминаются якобы имевшие место угрозы со стороны сотрудников OpenAI против соавтора, связанного с Anthropic — они отвергаются как ложные. Неясно, началась ли работа OpenAI над задачей до или после известия о прогрессе Buckmaster–Alpöge, что вызывает споры о мотивации ускорения. При этом подтверждено, что Buckmaster и Alpöge активно использовали Claude и Codex в процессе разработки. Многие считают, что инцидент приведёт к ужесточению ограничений на использование публичных LLM для конфиденциальных исследований. Рекомендуется избегать ввода черновиков доказательств в публичные интерфейсы до ясности условий использования. Предлагается разработать общепринятые нормы атрибуции и лицензирования при значительном вкладе LLM в математические доказательства.