Китайский ИИ решил давнюю математическую задачу без участия человека

Китайский ИИ решил сложную математическую задачу без участия человека.
Нейросеть решила открытую алгебраическую гипотезу, сформулированную американским математиком Дэном Андерсоном в 2014 году.
Система ИИ использует два основных компонента: Rethlas (рассуждающий агент на естественном языке) и Archon (агент формализации).
Rethlas обращается к поисковой системе Matlas для изучения стратегий решения, имитируя мыслительный процесс математика.
Когда Rethlas находит потенциальное доказательство, Archon преобразует его в проект для интерактивного доказательства теорем Lean 4.
Ключевое отличие нового инструмента от предыдущих нейросетей - он не нуждается в пристальном надзоре со стороны человека.
Математические доказательства требуют полной строгости, а большие языковые модели склонны к галлюцинациям и ненадежны.
Новая система способна выполнять математические задачи быстрее любого человека.
Работа ученых иллюстрирует новую парадигму математических исследований, в которой неформальные и формальные системы рассуждения работают в тандеме.