Astra от OpenAI решила 10 задач, над которыми математики бились десятилетиями: доказательства уже на GitHub

Внутренняя версия Astra, следующего крупного семейства моделей OpenAI, решила 10 открытых задач математики и теоретической информатики - каждая стояла минимум 10 лет, большинство дольше. Компания впервые подтвердила модель 1 августа 2026 года и выложила все доказательства в открытый репозиторий. Заглавный результат: явная конструкция несофической группы, вопрос стоял с 1999 года, когда Михаил Громов ввёл понятие софичности.

Проверка изменилась. Контрпример к unit distance от внутренней модели OpenAI в мае 2026-го девять внешних математиков проверяли вручную. Теперь за них работает Lean: система машинной проверки доказательств сверяет каждый шаг вывода, и все 10 результатов идут с такими сертификатами.

Перепроверить можно у себя: качай репозиторий openai/ten-proofs с GitHub, ставь Lean 4.32.0 с mathlib и запускай lake exe cache get, затем lake build All. Незакрытых шагов sorry в репозитории ноль.

В десятку также вошли упаковка сфер в высоких размерностях, гипотеза жёсткости Конна и многоцветные числа Рамсея. Три задачи пришли из каталога Эрдёша, включая проблему 183 о числах Рамсея.

Цена вопроса. Токены на генерацию всех 10 решений стоили бы около $2000 по API-тарифам GPT-5.6 Sol. Разработка модели и проверка результатов людьми в эту сумму не входят.

В соавторах 249-страничного манускрипта людей нет: OpenAI настаивает, что аргументы целиком принадлежат модели, а сотрудники лишь довели вывод до формата исследовательских статей и отвечают за точность.

Сама OpenAI признаёт: другие крупные задачи модель не взяла, и больших бюджетов на каждую не тратили. Нейт Сильвер добавляет, что контрольной группы не было - тот же бюджет не дали ни математикам-людям, ни модели GPT-5.6 Sol.

Перед релизом Astra первой из моделей OpenAI пройдёт новый федеральный процесс проверки безопасности США: он уже замедлял выкатку GPT-5.6.