ИИ автономно решил открытую математическую проблему и завершил крупномасштабную формальную верификацию

Исследовательская группа AI4Math Пекинского университета впервые в Китае использовала автономную ИИ-систему для решения открытой проблемы в коммутативной алгебре — гипотезы Андерсона, предложенной в 2014 году, и успешно завершила её формальную верификацию, состоящую примерно из 19 000 строк кода на Lean 4.

Прорыв стал возможен благодаря созданной командой системе с двумя ИИ-агентами: Rethlas, который с помощью семантического поиска по миллионам математических утверждений нашёл, казалось бы, не связанную теорию для построения контрпримера, и Archon, который преобразовал доказательство в код, самостоятельно обнаружил логические пробелы в первоначальном подходе, переработал стратегию доказательства и нашёл эквивалентные пути, когда нужные математические концепции отсутствовали в библиотеке Lean.

Достижение, основанное на трёхлетней работе и междисциплинарном сотрудничестве, не только решает конкретную математическую проблему, но и подтверждает новую парадигму исследований, объединяющую ИИ и математику. Учёные призывают поддерживать такие инновации для решения крупных научно-технических задач.