Список результатов охватывает несколько разделов чистой математики и теоретической информатики. Главный — явное построение несофичной группы: Astra оттолкнулась от группы единиц алгебры Ливитта, скомбинировала расширяющие графы Куна — Тома и группу Томпсона V и довела рассуждение до противоречия, впервые доказав само существование несофичных групп — вопрос, который оставался открытым с 1999 года, когда Михаил Громов сформулировал понятие софичности.
Среди других результатов — новая верхняя оценка плотности упаковки сфер в высоких размерностях (первое улучшение общей границы за 48 лет, приближение к порогу Кона — Элкиса), опровержение гипотезы жёсткости фон Неймановых алгебр Конна, доказательство гипотезы об объёме Эрхарта и решение трёх задач из каталога Пола Эрдёша, включая задачу 183 о мультицветных числах Рамсея.
Все десять доказательств оформлены как сертификаты в системе формальной верификации Lean 4 и выложены в репозитории openai/ten-proofs на GitHub под лицензией Apache 2.0 — по одному .lean-файлу на результат (NonSoficGroup.lean, ConnesRigidity.lean, SpherePacking.lean и т.д.). Счётчик незакрытых мест («sorry») в репозитории равен нулю — это означает, что каждый шаг во всех десяти доказательствах формально проверен компьютером, а не полагается на неформальную (и потенциально ошибочную) человеческую проверку, как большинство публикуемых математических доказательств.
Astra — та же внутренняя модель OpenAI, которую компания ранее впервые классифицировала как модель с «критическим» уровнем риска и придержала от полноценного релиза. Математические доказательства — это демонстрация возможностей той же системы в контролируемой, формально проверяемой области, где у модели физически нет способа обмануть проверку: Lean-компилятор либо принимает доказательство, либо нет. Для рынка ИИ это одна из первых по-настоящему бесспорных демонстраций научного открытия, сделанного моделью, а не просто пересказа существующих знаний.
Для российских разработчиков LLM (Сбер, Яндекс, T-Bank) это ориентир нового класса бенчмарков — не human-level знания, а способность двигать границу открытого математического знания, — и напоминание о разрыве в масштабе вычислений и исследовательских бюджетах между лабораториями уровня OpenAI и российскими командами.