В начале августа OpenAI в блоге, посвящённом математике, незаметно анонсировала новую модель Astra. При этом компания не привела стандартных бенчмарк-результатов, а продемонстрировала способности модели иначе: Astra смогла решить 10 сложных задач из области математики и теоретической информатики, которые долгое время оставались нерешёнными.
OpenAI описала Astra лишь как «следующую основную модель», не уточнив её точное место в линейке продуктов. По наблюдениям СМИ, модель может быть версией GPT-5.6, GPT-6 или представлять собой совершенно новый продукт. По информации The Information, Astra способна выполнять длительные задачи. Глава OpenAI Сэм Альтман недавно демонстрировал модель федеральным чиновникам.
Решённые задачи охватывают разные области: от многомерной геометрии до теории кодирования, от теории групп до квантовой сложности. Одна из важнейших находок — построение первого известного «не sofic-группы» (non-sofic group), что стало ответом на вопрос, остававшийся открытым почти 27 лет. Также модель опровергла гипотезу Алена Коннеса (1980) и решила три задачи из известного сборника задач Эрдеша.
Особенность публикации результатов — использование Lean-доказательств. Каждое решение Astra сопровождается машинно-читаемым доказательством, которое можно проверить с помощью Lean 4. Эти доказательства опубликованы на GitHub. Такой подход позволяет любому человеку самостоятельно проверить корректность доказательств без необходимости ждать экспертной оценки. Однако остаётся вопрос соответствия формализованного утверждения исходной математической задаче — это требует участия математического сообщества.
Этот подход отличается от предыдущих действий OpenAI. Например, в октябре 2025 года бывший вице-президент OpenAI Кевин Вейл заявил в X о решении GPT-5 десяти задач Эрдеша, но математик Томас Блум из Манчестерского университета обнаружил, что модель лишь нашла готовые решения из литературы. Теперь же Блум назвал результаты Astra «большой новостью».
OpenAI также учла положения Leiden Declaration (опубликованного в июне), где говорится о необходимости прозрачности при использовании AI в науке. Компания прямо указала, что математические идеи исходят от Astra, а не от людей, обрабатывавших материалы.
При этом, по словам исследователя OpenAI Ноама Брауна в X, Astra не смогла решить ни одной из «задач тысячелетия» (за решение каждой из них Математический институт Клэя предлагает награду в 1 млн долларов). Однако он отметил, что на решение текущих задач было потрачено относительно мало вычислительных ресурсов, и у модели есть значительный потенциал для дальнейшего развития.
Подписаться в Макс
