Содержание
Почему формально проверенный контрпример Astra мог не опровергнуть гипотезу Конна
Одно из десяти математических достижений, которые OpenAI приписала своей новой модели Astra, оказалось под вопросом. Математик Дженни Лоррейн Нильсен опубликовала разбор заявленного опровержения гипотезы Конна и указала: построенный нейросетью контрпример не удовлетворяет важному условию исходной задачи.
В чём обнаруженная проблема
В анонсе OpenAI говорилось, что Astra построила две неизоморфные группы со свойством (T), чьи групповые алгебры фон Неймана изоморфны. Нильсен не утверждает, что сами вычисления или формализация в Lean обязательно неверны. По её анализу, обе группы имеют нетривиальный центр и поэтому не являются ICC-группами — а именно это условие входит в стандартную формулировку гипотезы Конна.
Иными словами, формальный сертификат может корректно подтверждать доказанный внутри него результат, но этот результат относится к объектам за пределами исходной гипотезы. Это принципиальная разница: модель могла решить близкую формальную задачу, не предоставив контрпример к той математической проблеме, которую OpenAI назвала опровергнутой.
Что это меняет в анонсе OpenAI
OpenAI 31 июля представила десять результатов Astra и отдельно заявила, что берёт ответственность за их корректность. На момент публикации этой новости официальный пост по-прежнему перечисляет «опровержение гипотезы Конна» среди достижений модели и не содержит заметного исправления.
Новый разбор касается одного из десяти результатов и сам по себе не опровергает остальные работы Astra. Но он показывает важное ограничение AI в науке: проверка доказательства в Lean подтверждает соответствие формально заданной теореме, однако не гарантирует, что формулировка точно совпадает с неформальной задачей и принятыми в научном сообществе условиями.
Почему это важно
Для пользователей и бизнеса история — напоминание не путать формальную корректность с корректной постановкой задачи. Даже сильные reasoning-модели требуют экспертной проверки исходных допущений, особенно когда результат подаётся как научное открытие. Сейчас корректнее говорить, что одно из заявлений OpenAI о результатах Astra оспорено и ожидает реакции компании и более широкой оценки математиков.