Математики пытаются разобраться в масштабной публикации OpenAI
OpenAI представила почти 400 сгенерированных ИИ результатов в более чем 700 рукописях, однако значительная часть материалов пока не прошла формализацию и проверку
Один основной источник · Как мы проверяем новости
Что произошло
OpenAI опубликовала почти 400 результатов, созданных ИИ, в более чем 700 математических рукописях. Коллекция охватывает широкий круг дисциплин, а для ее навигации компания подготовила отдельные рекомендации по работе с репозиторием GitHub.
Более трех десятков математиков, опрошенных The Verge, назвали масштаб публикации ошеломляющим и заявили, что даже первичное понимание всех материалов может занять годы.
Проблемы с проверкой
Часть рукописей содержит формализации в Lean — языке программирования и средстве проверки доказательств, позволяющем подтверждать результаты вычислительно. Однако OpenAI указала, что материалы находятся на разных этапах проверки, а формализована лишь часть коллекции.
Исследователи также сообщили, что качество проверяемых доказательств различается, а утверждения, подтвержденные кодом, не всегда точно соответствуют тезисам сопроводительных рукописей.
Почему это важно
Математикам приходится выбирать между самостоятельным изучением большого массива потенциально ошибочных материалов и ожиданием независимой проверки. Kevin Buzzard из Imperial College London отметил, что среди многочисленных теорем в области алгебраической теории чисел сразу выделились лишь около шести, причем немногие из них выглядели формально проверенными в Lean.
Собеседники The Verge опасаются, что OpenAI может перейти к новым публикациям до того, как научное сообщество успеет разобраться с нынешней коллекцией.
Источники
Один основной источник. Как мы проверяем новости
