26 октября 2026
Axiom Math выпустила полную формализацию CFSG в Lean за 24 дня
Axiom Math открыла код и материалы по полной компьютерно проверенной формализации классификации конечных простых групп (CFSG) в Lean. По данным компании, на проект ушло 24 дня: команда инженеров и математиков координировала десятки ИИ-агентов, разбив работу на 108 этапов и около 380 более мелких задач.
Масштаб здесь сам по себе необычный. Формализация занимает около 43,1 млн строк Lean; исходный корпус доказательств опирается примерно на 15 000 страниц, более 500 статей и работу около 100 математиков. Проверку каждой логической части выполняет ядро Lean, то есть итог валидирует не ещё одна модель, а детерминированный верификатор.
Axiom также пишет, что проект выявил 34 существенных отклонения от опубликованных доказательств, включая проблему в участке вокруг Unbalanced Group Theorem. При этом важно различать две вещи: машинная проверка подтверждает корректность формализованной версии, но не автоматически гарантирует её полную эквивалентность исходной неформальной формулировке.
Для разработчиков агентных систем это скорее кейс по оркестрации и контролю качества, чем просто новость из математики: генерацию можно распараллелить между многими исполнителями, а приёмку замкнуть на строгий проверяющий контур. Публичных API или цены для этой системы Axiom не раскрывает.