В мире технологий произошел значимый прорыв: команда ученых из Пекинского университета разработала искусственный интеллект, который самостоятельно решил математическую задачу, предложенную более десяти лет назад. Эта задача была поставлена бывшим профессором Университета Айовы Дэном Андерсоном, который ушел из жизни в 2022 году.
Их двухагентная система, названная Rethlas, использует методы естественного языка и формальной верификации, чтобы не только решить проблему, но и подтвердить свои выводы. Исследователи утверждают, что с помощью этой системы они смогли решить открытую задачу в области коммутативной алгебры и автоматически формализовать доказательство без какого-либо человеческого вмешательства.
Команда под руководством профессора Дун Бина объединила экспертов в области математики и искусственного интеллекта, что позволило им достичь впечатляющих результатов. Они отметили, что их система выполняет математические задачи быстрее, чем люди, и может самостоятельно выполнять работу, которая обычно требует сотрудничества специалистов из разных областей.
Это исследование подчеркивает растущую роль искусственного интеллекта в математике, особенно с учетом недавних достижений в области больших языковых моделей (LLMs). Например, система Google Gemini Deep Think достигла золотого стандарта на Международной математической олимпиаде 2025 года.
Несмотря на успехи, команда отметила, что использование ИИ для решения исследовательских задач все еще требует значительного человеческого контроля. Они предложили новый подход, который сочетает в себе агента для естественного языка и формализующего агента, что позволяет значительно автоматизировать процесс математических исследований.
В результате их работы была успешно решена задача о квазиконечных Нетеровых локальных кольцах, что является важным понятием в коммутативной алгебре, служащей основой для современной алгебраической геометрии и теории чисел. Интересно, что вся формализация была завершена за 80 часов работы системы, и единственным вмешательством человека было скачивание платных файлов, которые агент не смог получить самостоятельно.
Таким образом, исследование демонстрирует, как ИИ и математика могут эффективно сотрудничать, открывая новые горизонты для автоматизации математических исследований.