Axiom Math объявила 26 октября о полной формализации классификации конечных простых групп в Lean — языке, позволяющем компьютеру проверять логические шаги доказательства. По отчёту компании, десятки ИИ-агентов под руководством математиков и инженеров за 24 дня подготовили около 43,1 млн строк кода.

Классификация описывает базовые строительные блоки конечных групп — математических объектов, выражающих симметрии. Её доказательство создавали десятилетиями; оно разбросано примерно по 15 тысячам страниц. Формализация связывает эти аргументы в явно проверяемую цепочку, которую можно использовать в дальнейших работах.

Агенты распределяли задачи, искали готовые результаты и писали доказательства. Люди разбирали математические препятствия и поддерживали вычислительную инфраструктуру. Первые попытки иногда добавляли недоказанные предпосылки: такие участки пришлось удалять и переделывать. Поэтому число написанных строк само по себе не означало завершённой проверки.

Авторы сообщают о 34 существенных расхождениях с опубликованной литературой. Один случай разобран в препринте от 27 октября: контрпример обнаружился в промежуточном рассуждении одного из доказательств теоремы о несбалансированных группах. Он не опровергает саму теорему, у которой есть другие доказательства; работа предлагает альтернативное обоснование для нужного случая.

Репозиторий открыт под Apache 2.0. В описании проекта заявлены отсутствие непроверенных заглушек и использование трёх стандартных аксиом Lean. Полную сборку редакция не воспроизводила. Lean проверяет вывод из формальных определений, а соответствие этих определений исходной математической задаче проверяют люди. Как и в истории с теоремой Ферма, главный результат здесь — перевод существующей математики в проверяемый код; классификация остаётся достижением создавших её математиков.