Математики будут разбирать доказательства OpenAI годами: Lean-проверка есть примерно у 42%

Больше трёх десятков математиков, с которыми говорили журналисты, назвали происходящее «ошеломляюще» и «чистым безумием». Причина в объёме: поток результатов обрушился на поле за одну неделю, и разбирать его придётся годами.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Что выложили. Репозиторий openai/math содержит 719 рукописей, сгруппированных в 372 семейства. Начать можно с overview.pdf, там описаны семейства. Поиск отдельной работы идёт через CONTENTS.md, а инструкция по проверке лежит в ComparatorChallenges/README.md. Lean это язык, на котором компьютер проверяет доказательство шаг за шагом.

Как получено. DataCamp пишет, что модели поставили около 4000 открытых задач. На результат в среднем ушло около трёх часов ChatGPT Pro thinking time, и большая часть результатов получена одной фиксированной процедурой. Промпты, расход вычислений по каждой задаче и название модели не раскрыты, а это расходится с рекомендациями консультативной группы.

Раньше на такую задачу уходили годы. Бакмастер и Альпёге почти год работали над доказательством для Навье–Стокса. По данным MIT Technology Review, OpenAI решила проблему за несколько дней, запустив 10 000 агентов одновременно на сумму в миллионы долларов.

Спорная часть. Теренс Тао (UCLA) назвал предварительное решение задачи чисто ИИ-методами без полной прозрачности процесса. По его словам, это может «загрязнить этот процесс до такой степени, что он станет чистым минусом для прогресса математики в целом».

Дальше вопрос в том, сколько из 372 семейств результатов получат машинную проверку в Lean.