Axiom Math выпустила 43,1 млн строк Lean-доказательства классификации групп

Axiom Math 27 октября 2026 года объявила о первом полном компьютерно-проверенном доказательстве классификации конечных простых групп. Проект на 43,1 млн строк Lean, 2,05 млн деклараций и 715 источников выполнили рои ИИ-агентов за 24 дня; в ходе работы найдено 34 заметных отклонения от опубликованных доказательств.

• 43,1 млн строк Lean, 2,05 млн деклараций и 715 источников в корпусе
• Проект занял 24 дня, работа шла через 108 вех и около 380 задач
• Найдено 34 заметных отклонения от публикаций, включая ошибку в квазитонких томах
• Код под лицензией Apache-2.0, сборка проверяется через lake build менее чем за 24 часа