OpenAI решила 10 математических задач за $2000 каждая: как проверить результат самому
OpenAI потратила меньше $2000 на модель Astra и решила 10 нерешаемых десять лет задач. Разбираем, что реально проверяемо, а что на словах.
OpenAI выпустила отчёт о десяти продвижениях в математике и теоретической компьютерной науке, полученных внутренней версией модели Astra. Заявка звучит громко: задачи не двигались минимум десять лет, а на каждую решение стоило меньше $2000 в токенах GPT-5.6 Sol. Если вы работаете с AI-инструментами и хотите отличить реальный прорыв от красивой презентации, у вас есть шанс проверить это самостоятельно — компания открыла код и формализации доказательств.
Ниже — не пересказ пресс-релиза, а инструкция, куда смотреть, чтобы составить собственное мнение, а не купиться на заголовки.
Что именно опубликовано
OpenAI выложила три артефакта, и это важно понимать раздельно, потому что у них разный уровень доверия.
Первый — репозиторий openai/ten-proofs с формализациями результатов на Lean 4 (язык для формальной верификации доказательств, где каждый шаг проверяется машиной, а не человеком на глаз). Это самый надёжный источник: если Lean принимает доказательство, значит логическая цепочка корректна с точки зрения формальной системы.
Второй — научная статья, описывающая сами решения человеческим языком: постановки задач, идеи доказательств, контекст.
Третий — дополнительный PDF, сгенерированный самой моделью. В нём модель «реконструирует», как строилось доказательство, опираясь на неопубликованные цепочки рассуждений (reasoning traces). Это самый шаткий из трёх документов: он не является записью реального процесса, а пересказом модели о себе самой, без доступа к оригинальным логам.
Почему прозрачность здесь неполная
OpenAI не публикует промпты, которыми модель наводили на задачи. Без промптов невозможно оценить, сколько direction задавал человек, а сколько модель нашла сама. Формулировка задачи в отчёте — «мы не ищем низко висящие фрукты, нам нужны настоящие сложные находки» — это цитата из похожего эксперимента Anthropic с Mythos Preview (там компания потратила $100 000 на токены, ища криптографические уязвимости у Claude). Похожая риторика у обеих лабораторий наводит на мысль, что степень человеческого кураторства в обоих случаях выше, чем создаётся впечатление в заголовках.
Второй пробел — статистика неудач. OpenAI сообщает цену успешных решений, но не говорит, сколько задач стоили те же $2000 и не привели ни к какому результату. Без знаменателя цифра «$2000 за прорыв» — это только числитель. Возможен survivorship bias (систематическая ошибка выжившего): показывают десять побед, но молчат про сотню попыток, которые ничем не закончились.
Как самому оценить достоверность
Если вы хотите разобраться без слепого доверия к пресс-релизу, идите по такому порядку.
Сначала откройте репозиторий openai/ten-proofs и посмотрите на формализации Lean 4 напрямую — независимо от того, читаете вы Lean свободно или нет, важно, что файлы существуют и структурированы как настоящие формальные доказательства, а не текстовые заглушки.
Затем сравните формулировки задач в статье с тем, что реально считается открытыми проблемами в соответствующей области (геометрия, криптография, теория сложности). Проверьте, действительно ли результат «не двигался десять лет» — это легко сверить по цитируемости и датам последних публикаций по теме.
После этого прочитайте LLM-сгенерированный PDF критически: ищите места, где модель описывает "инсайт" или "поворотный момент" — такие формулировки без доступа к исходным логам рассуждений нельзя проверить, это литературная реконструкция, а не протокол эксперимента.
Наконец, обратите внимание на масштаб: десять задач — это не революция в математике, а точечный демонстрационный кейс. Оценивайте его как один эксперимент, а не как доказательство общей способности ИИ решать открытые проблемы.
Что это значит для практики
Терренс Тао, реагируя на подобные результаты ещё в июне в интервью IEEE Spectrum, предложил термин «большая математика» (big mathematics): не одиночный гений с доской, а децентрализованное сотрудничество людей и машин, где творческую часть задачи берёт человек, а техническую рутину — модель. Это рабочая модель, применимая не только к чистой математике, но и к любой инженерной задаче, где есть формальная проверка результата: тесты, компиляторы, верификаторы типов.
Практический вывод для разработчиков и продуктологов: если в вашей области есть строгий верификатор (компилятор, набор тестов, формальная спецификация), у LLM появляется реальный шанс генерировать полезные результаты, потому что ошибку легко отфильтровать автоматически. Без верификатора вы получаете красивый текст без гарантии корректности — ровно то, чем рискует быть тот самый LLM-сгенерированный PDF-пересказ.
Другой практический сигнал — экономика. Цена в $2000 за токены на одну задачу говорит о том, что подобные эксперименты пока доступны только компаниям с прямым доступом к внутренним, ещё не выпущенным моделям (Astra, GPT-5.6 Sol — это внутренние обозначения, не публичные продукты). Обычному пользователю такой уровень мощности сейчас недоступен ни по цене, ни по доступу.
Где ломается доверие к таким анонсам
Главный риск — путать формальную верификацию (Lean принял доказательство) с прозрачностью процесса (мы знаем, как модель к нему пришла). Первое проверяемо объективно, второе — не публикуется намеренно.
Второй риск — реагировать эмоционально, а не аналитически. В математическом сообществе уже пошла волна тревоги: математик Кирвин Хэмпшир написал эссе «Тёмная ночь математики» о «глубоком духовном кризисе» из-за предыдущих, менее значимых результатов ИИ. Сравнения с моментом Deep Blue (победой шахматного движка над Каспаровым в 1997 году) звучат постоянно, но полезнее не искать драму, а смотреть на конкретные артефакты: код, доказательства, метрики.
Третий риск — обобщать один точечный кейс на всю область. Десять решённых задач за одну публикацию — это сигнал о возможностях, а не статистика о надёжности метода в широком применении.
Что попробовать дальше
Откройте openai/ten-proofs и посмотрите хотя бы на одну формализацию Lean 4 целиком — это займёт пятнадцать минут и даст более честное представление, чем любой пересказ в новостях.
Сравните подход OpenAI с методом Anthropic из истории с Mythos Preview: обе компании используют похожую риторику про «не низко висящие фрукты» — это подсказка, что оба эксперимента построены на похожей идее целевого промптинга под сложные задачи, а не на свободном исследовании модели.
И если вы работаете в области с формальным верификатором — компилятором, тестовым фреймворком, системой типов — присмотритесь к идее Терренса Тао про «большую математику»: возможно, у вас в проекте уже есть та самая инфраструктура, которая делает LLM полезным инструментом, а не генератором красивого текста без гарантий.
Источники
Читайте также
Комментарии
Пока никто не написал. Будьте первым.