Hacker News Digest

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

Несмотря на прогресс, большинство проблем на переднем крае математики остаются нерешёнными — пространство задач бесконечно, а их сложность неограниченна. Поэтому будущее математики — «Math 2.0» — должно выходить за рамки простого поиска доказательств. Нужно смещать фокус с количества на качество: использовать ИИ для выявления новых принципов, методов и инсайтов, улучшать существующие доказательства, исследовать «окрестности теорем», строить интерпретируемые и безопасные открытые математические модели. Примеры включают Maththon — студенческий марафон по улучшению доказательств, IEANTN — динамическую сеть результатов в аналитической теории чисел, и ablation studies — проверку устойчивости théorems при удалении посылок. Главное препятствие для Math 2.0 — не технологии или культура, а воображение: умение видеть, как ИИ может углубить понимание, а не просто автоматизировать поиск.

Кризис в математике — не технологический, а культурный: утрата смысловых стимулов, идентичности и институциональных механизмов признания. Математики теряют традиционные пути к признанию — решение открытых задач, коллаборации, приглашения на конференции — из-за того, что AI-лишает их этих возможностей. AI-доказательства часто не интегрируются в математическую «кодовую базу», поскольку строятся с нуля, без опоры на существующие теории, что делает их бесполезными для дальнейшего развития. Спор: одни считают, что понимание механизма AI не требуется для его применения (как в медицине), другие — что понимание остаётся фундаментальной целью чистой математики, и его отказ разрушает её суть. Сравнение с программированием: математики сталкиваются с доказательствами, которые не могут интерпретировать, как разработчики с непонятным кодом — это эволюция профессиональной реальности. Современная наука (медицина, инженерия) уже работает с полуэмпирическими моделями (SPICE, анестезия), и это не мешает использованию. Критика Тао за пример с раком — проекция страха; его аргументы о стерильности поля и разрушении путей признания остаются релевантными. Математика как культура переживает трансформацию: ценности, стимулы и иерархии изменятся, но сама математика выйдет сильнее. AI не заменяет понимание, а меняет его природу: люди могут переключиться с решения на анализ, интерпретацию и улучшение AI-доказательств — удовольствие от математики в понимании, а не в решении. Опасение: AI может генерировать «бесполезные» доказательства (экспоненциально сложные, без инсайтов), отвлекая от глубоких закономерностей. Эпистемологическая проблема: если AI «бегает» по доказательству, но человек не видит этапов, как доверять результату? Это не решается только формальной верификацией. AI уже меняет практику: исследователи переписывают гранты, бросают годы работы, чувствуют себя ненужными — реальное поведенческое смещение. Тао не против AI — он предупреждает, что человечество может перестать развивать «путь к свету», а будет только добираться до «светильников» без понимания их работы. Сравнение с программированием: «vibe proving» AI может привести к хаотичному, неподдерживаемому математическому «коду», как «vibe coding» разрушает качество ПО. Наука всегда адаптировалась к новым инструментам (калькуляторы, компьютеры); кризис — это переход, а не конец, но адаптация требует осознанности. Совет: математикам следует переключиться с решения задач на анализ, рефакторинг и объяснение AI-доказательств — это новая форма творчества, сохраняющая человеческую роль.

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

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

Математик и его коллега Левант Альпоге объявили о достижении конечного времени взрыва с гладким принуждением для трёх систем: уравнения несжимаемой пористой среды, системы Буссинеска и трёхмерных уравнений Эйлера. Они считают, что также получили взрыв для гипо-диссипативных уравнений Навье-Стокса, но не публикуют этот результат, поскольку проверка в 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 в математические доказательства.