ИИ за несколько дней решил задачу, над которой математики бились больше 10 лет.

Китайский искусственный интеллект самостоятельно решил открытую проблему, предложенную более десяти лет назад американским математиком, сообщает команда разработчиков из пекинского университета. Гипотезу о свойствах квазиполных нетеровых локальных колец сформулировал бывший профессор университета айовы Дэн Андерсон в 2014 году.
Исследователи двух агентов ИИ объединили. Один выполняет рассуждения на естественном языке, другой занимается формальной машинной верификацией.

"Используя Этот Фреймворк, мы Успешно Решили Открытую Проблему в Коммутативной Алгебре", - пишут они.
Первый компонент - агент неформальных рассуждений Rethlas с поисковой системой Matlas. Второй - агент формальной верификации Archon с поисковой системой Leansearch, превращающий доказательства в верифицированные проекты на Lean 4 с библиотекой Mathlib. Система нашла контрпример, опровергающий гипотезу, и проверила его за 80 часов. Единственным вмешательством человека стала загрузка файлов с платного доступа.
"Наши Результаты Показывают, что для Реальной Открытой Проблемы в Математике Агенты Неформальных Рассуждений и Формальные Агенты Могут Эффективно Сотрудничать", - заключается в статье.