OpenAI выложила 722 работы своей модели по открытым задачам математики: что это и при чём тут ChatGPT

6 октября OpenAI опубликовала большую подборку математических результатов, которые получила её внутренняя невыпущенная модель: 722 рукописи, сгруппированные в 372 «семейства». Всё лежит в открытом репозитории на GitHub, многие доказательства переведены на Lean, чтобы их мог проверить компьютер. Это исследовательский релиз, а не новая функция: в ChatGPT ничего не появилось. Анонс - в блоге OpenAI.

Что именно выложили

• 722 рукописи в 372 семействах. Семейство объединяет основной результат, следствия и альтернативные доказательства, каждое отнесено к своему разделу математики.
• Около 4000 задач. Столько модели дали за время проверки, в каталог попали только достаточно значимые результаты.
• Три часа «размышлений» Pro. В среднем один результат потребовал столько вычислений, сколько три часа работы ChatGPT Pro в режиме рассуждений, но на этой внутренней модели.
• 10 конспектов хода мысли модели, среди тем - показатель иррациональности числа пи и гипотезы Малера.

Зачем Lean и почему GitHub

Lean - язык, на котором доказательство записывают так, что его правильность проверяет программа, а не рецензент вручную. OpenAI обещает добавлять такие версии по мере готовности. Публиковать результаты компания решила по советам независимой группы математиков при Институте перспективных исследований в Принстоне (AGMAI).

Где подвох

Не всё проверено машиной: формализованы многие, но не все рукописи. Есть исключения из общей процедуры: работа о дзета-функции Римана и гипотеза Ходжа для одного класса абелевых многообразий получены иначе, а один текст про дзета-функцию люди отредактировали для читаемости.

Фон тоже непростой. По данным The Verge, математики критикуют OpenAI за то, как она объявляет такие результаты, а AGMAI призывала не превращать их в рекламу моделей. Историю со спором вокруг задачи Навье-Стокса мы разбирали отдельно.

Что это значит для нас

Для подписчиков ChatGPT сегодня ничего не меняется. Модель, которая получила эти результаты, недоступна ни в одном тарифе. OpenAI пишет только, что работает над ответственным выпуском этой модели, без сроков и без названия. Из того, что уже вышло, свежее всего GPT-6.1 Sol: она доступна с тарифа Plus, но только в ChatGPT Work и Codex.

Российская карта на сайте OpenAI не проходит. Подписка ChatGPT Plus и Pro есть в нашем каталоге, оплата картой РФ или СБП.