Омри Вайнштейн — теоретик информатики, тот самый тип, кто годами работает над одним вопросом и обычно с первого взгляда понимает, настоящим ли доказательством в его области пахнет или лишь желаемым. На этой неделе он написал, что передумал насчёт вещи, которую не ожидал передумывать.
«Даже недавний прорыв OpenAI в области теоремы Эрдёша не убедил меня, что LLM способны вести общие математические исследования, — написал он. — Это изменило моё мнение».
Изменения добилась короткая, почти неприметная цепочка, выстроенная его бывшим коллегой из Колумбийского университета Бинхуэем Пэном вместе с Жуньчжоу Тао, Стивеном Ваном и Ханьтао Юем. Направленная на девять открытых задач, она решила их. Не упражнения, замаскированные под исследования, а опубликованные открытые вопросы, некоторым из которых больше десяти лет, взятые из списков основных конференций области. Один из них, по словам Вайнштейна, не давал ему спать два года.
Как работает конвейер
Если убрать обрамление, метод почти обыденный, и именно это делает его впечатляющим. Один этап играет роль доказывающего: получив открытую проблему, он выписывает полный аргумент. Второй этап играет роль проверяющего, читает этот аргумент как рецензент, выискивает шаг, который не следует, случай, который пропущен, лемму, которая негласно принята, а не доказана, и возвращает возражения. Доказывающий правит. Цикл повторяется. Когда проверяющий перестаёт находить дыры, подключается человек.
Сами доказательства сгенерировал GPT-5.5 Pro. Описания собраны с помощью Claude Code, запущенного на Claude Opus 4.8, затем прочитаны, исправлены и утверждены авторами. Для алгебраических результатов команда пошла дальше и формализовала доказательства в Lean 4 с помощью собственной автоматической цепочки, чтобы помощник доказательств (а не языковая модель и не перегруженный рецензент) подтвердил, что каждая строка верна. Этот последний шаг весит больше, чем кажется. Формализованное доказательство — вопрос компиляции, а не вкуса. Оно либо компилируется, либо нет.
Девять проблем
Конкретные детали — это суть, поэтому вот полный список.
| Проблема | Источник |
|---|---|
| Перемешанный SGD и неравенства SS-RS-GD | Открытая проблема COLT 2021 |
| Обучение квантовых схем с измеряемым выходом (частично) | Открытая проблема COLT 2015 |
| Невзвешенный отбор данных для линейной регрессии | Открытая проблема COLT 2025 |
| Надёжная оценка условной вероятности | Открытая проблема COLT 2010 |
| Устойчивость к атакам при онлайн-сэмплинге по leverage-score | FOCS 2023 |
| Кольца с конечным проводником против квазикогерентных колец | Теория коммутативных колец |
| Гипотеза Кахена-Фонтаны-Фриша-Глаза | Теория коммутативных колец |
| Целочисленные полиномы над алгебрами | Теория коммутативных колец |
| Вопрос о дополнении замощения | Проблема Эрдёша 477 |
Ряд честных оговорок стоит добавить к этой таблице. Результат квантового обучения — частичное, а не полное решение. Речь идёт о специализированных задачах, понятных лишь нескольким десяткам исследователей в каждой области, а не о гипотезе Римана. И каждый текст перед публикацией вычитывал человек. Ничего из этого не скрывается; всё есть в отчётах самих авторов. Но это не отменяет главного факта: машина выдала математические идеи, которые решили задачи, над которыми тщетно бились внимательные специалисты.
Почему скептик изменил своё мнение
Даже недавний прорыв Эрдёша у OpenAI не убедил меня, что LLM способны вести полноценные математические исследования. Этот результат меня переубедил. С помощью хитрого цикла «доказывающий — проверяющий» на базе LLM удалось решить девять серьёзных открытых задач теоретической информатики, включая одну, которая не давала мне спать два года.
Omri Weinstein
Поддержка от людей, продающих технологию, ничего не стоит. Здесь речь не о таком случае. Вайнштейн не работает в лабораториях, он уже изучил самый разрекламированный недавний результат и нашёл его недостаточным, и у него был личный интерес в исходе. Один из девяти вопросов касался его собственной области. Задача FOCS 2023 по состязательной устойчивости онлайн-выборки по leverage-score лежит прямо в сфере его работы — вопрос, который специалист узнаёт с первого взгляда и сразу понимает его сложность изнутри.
Контраст, который он провёл с эпизодом OpenAI и Эрдёша, заслуживает внимания. В конце 2025 года сотрудники OpenAI заявили, что их модели решили серию задач из знаменитого списка Пола Эрдёша. Большая часть этих решений оказалась уже существующей в литературе — их просто пометили как открытые на популярном сайте отслеживания. Впечатляющий поиск, но не новая математика, и «прорывная» подача вызвала резкую публичную критику со стороны работающих математиков. Осторожный человек мог бы отнести это к хорошему поиску. Чего Вайнштейн не мог отнести к этой категории, так это свежего доказательства в своей собственной области вопроса, на который он сам лично не смог ответить.
Что здесь нового, а что — нет
Легко переоценить такой результат, и легко недооценить. Обоим стоит сопротивляться.
Ошибочное прочтение состоит в том, что математика теперь автоматизирована. Это не так. Люди выбирали задачи, направляли процесс, проверяли результат и писали итоговые статьи. Модели не проснулись однажды утром и не решили заняться перемешанным SGD. Конвейер — это инструмент, которым пользуются люди, уже знавшие, какие вопросы созрели.
Недооценка более соблазнительна для тех, кто десятилетие наблюдал, как заявления об ИИ раздуваются и сдуваются. Она говорит: симпатичная демонстрация, узкая область, идем дальше. Это упускает то, что произошло на самом деле. Идеи, несущие эти доказательства, конструкции, разборы случаев и неравенства, пришли от моделей. Верификация Lean и экспертами-людьми подтверждает, что идеи верны. Это языковая модель, вносящая несущую часть исследовательского результата, неоднократно, по задачам, выбранным именно потому, что их никто не решил, а не чат-бот, блефующий на устном экзамене.
Почему это на сайте о рисках ИИ
Расстояние между «ИИ может сдать сложный экзамен» и «ИИ способен создавать математику, недоступную экспертам» — именно то расстояние, которое Фонд пытается донести в каждой статье. Математика и теоретическая информатика — это фундамент, на котором всё строится, а не просто очередная область, которую захватит технология. Оптимизация, теория обучения и теория сложности — сырьё для следующей модели.
Система, способная осмысленно участвовать в открытых проблемах этих областей, в принципе может участвовать и в проектировании своего преемника. Эта фраза рекурсивное самосовершенствование. Исследования, ускоряющие исследования, — это разница между ровным подъёмом и спринтом, и авторы уже заявили, что планируют направить тот же конвейер на все области науки.
Работает ли метод повсеместно — почти не важно. Направление уже задано, и оно приближается быстрее, чем даже самые агрессивные прогнозы, казавшиеся таковыми в момент публикации хронология становится короче, и именно такие результаты тому причина Сценарий ИИ 2027 поставил автоматизированные исследования ИИ в центр своей истории именно по этой причине: как только машины начнут заниматься наукой, время ускорится.
Не является аргументом против решения открытых задач. Это аргумент о темпе. Люди, которые создают эти системы, сами публично говорят, что следующая способность уже близка, и она действительно появляется, и снова оказывается близка. Конвейер, который аспирант может запустить за выходные, теперь решает задачи, за которые раньше целая область отдавала высшие награды. Вопрос Фонд продолжает спрашивать единственное, что масштабируется вместе с возможностями: кто решает, насколько быстро всё идёт и на каких условиях. Пока ответа нет, и всё происходит как можно быстрее.