Новая ИИ-модель от OpenAI Astra решила 10 нерешённых математических задач. Об этом сообщается в блоге компании.
Решённые проблемы охватывают шесть направлений, включая высокоразмерную геометрию и криптографию на решётках. Главным достижением стало создание первой в истории явной конструкции несофической группы. Существование этого математического объекта исследователи активно обсуждали ещё с 1999 года.
Все десять доказательств были строго верифицированы с помощью инструмента проверки теорем Lean 4. На платформе GitHub уже опубликован 249-страничный манускрипт и машиночитаемые сертификаты. Подобный подход позволяет независимо проверить каждый шаг и полностью исключает ошибки ручной записи.
По оценкам самой компании, поиск всех решений обошёлся примерно в 2000 долларов по тарифам API. Математик Томас Блум назвал эти итоги «большой новостью», превосходящей прошлые достижения искусственного интеллекта. При этом он подчеркнул, что нейросети опираются на опыт людей и пока не заменят живых учёных.
Задачи из списка «премии тысячелетия» система Astra пока серьёзно не атаковала. Однако OpenAI планирует продолжать эксперименты и вскоре опубликует подробную техническую документацию. Ранее искусственный интеллект компании уже смог автономно опровергнуть гипотезу Эрдёша 1946 года.
Комментарии