Компания Axiom Math объявила о завершении компьютерной формализации теоремы классификации конечных простых групп, также известной как «Огромная теорема». Это один из крупнейших достижений математики XX века, и теперь он представлен как первое полностью компьютерно-проверяемое доказательство в форме Lean. По словам разработчиков, процесс занял 24 дня под руководством инженеров и математиков и охватил работу десятков ИИ-агентов, что позволило пройти от идеи к формализации доказательства. Источник сообщает, что проект заключил утверждение о компьютерной проверке, ранее не доводившейся до такого уровня детализации.

Исторический контекст включает самую длинную доказательскую цепь в математике. Исходное доказательство «Огромной теоремы» занимает порядка 15 тысяч страниц в более чем 500 научных статьях, над которыми трудились примерно сотня mathematicов. Вехи публикаций и авторы попыток систематизации начались ещё в 1960‑х годах: статья Уолтера Фейта и Джона Томпсона объёмом 255 страниц стала значительным этапом; позже достижения продолжились Дэниелом Горенштейном и, в 2004 году Майклом Ашбахером и Стивеном Смитом, что дало изложение длиной 1221 страница — всё это входило в так называемое доказательство первого поколения, над формализацией которого и работали специалисты Axiom Math.

При формализации агенты обнаружили 34 существенных расхождения с опубликованными работами и контрпримеры к утверждениям. Чтобы завершить проверку, исследователям пришлось исправлять часть рассуждений, разрабатывать новые математические аргументы и даже получить новый результат в теории групп. В работе участвовали эксперты по теории групп, знакомые с первоначальным доказательством. Авторы проекта назвали результат первым полным компьютерно-проверяемым доказательством теоремы классификации конечных простых групп.

В отчёте отмечается, что над проектом работали десятки ИИ‑агентов под руководством инженеров и математиков; объем кода, написанного на языке Lean, достиг около 43,1 миллиона строк. Так же указывается, что для завершения проверки пришлось доработать часть рассуждений и придумать новые аргументы, включая получение нового результата в теории групп. Ранее газеты сообщали о попытках проверить гипотезы экспоненциального времени и аналогичных вопросов в смежных моделях.