OpenAI решила 10 математических задач за $2000 каждая: как проверить результат самому

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 полезным инструментом, а не генератором красивого текста без гарантий.

Источники

• Simon Willison: Ten advances in mathematics and theoretical computer science