Внутренняя версия модели Astra от OpenAI совершила математический прорыв, решив 10 задач по математике и информатике, которые оставались открытыми более десяти лет. Результаты представлены в виде строгих доказательств, сообщает сайт infohub.kz.
Компания OpenAI опубликовала 249-страничный рукописный сборник и цифровые сертификаты Lean 4 для 10 нерешенных задач на платформе GitHub под лицензией Apache 2.0. Все доказательства, выведенные алгоритмом, успешно прошли формальную машинную проверку без единого пропуска в логических цепочках.
Среди решенных проблем — опровержение гипотезы Конна о жесткости, выдвинутой еще в 1980 году, построение доказательства существования несофической группы, а также решение задачи № 183 Пола Эрдёша, связанной с многоцветными числами Рамсея. Дополнительно Astra нашла решения в области упаковки сфер в многомерных пространствах, квантового повторения и сложности алгоритмов.
Новая ИИ-система Astra предназначена для длительной работы над сложными задачами путем координации работы нескольких агентов. Исследователь Ноам Браун отметил, что затраты на токены составили всего около $2000. Впрочем, всем представленным результатам еще предстоит пройти экспертную рецензию ученых.


