Axiom: «огромную теорему» о конечных простых группах проверили в Lean
Axiom: «огромную теорему» о конечных простых группах проверили в Lean Axiom Math выпустила первую полную машинно проверенную формализацию Classification of Finite Simple Groups — доказательства примерно на 15 000 страниц. За 24 дня инженеры и математики направили рои из десятков ИИ-агентов: получилось около 43,1 млн строк Lean. Формализация вскрыла 34 заметных отклонения от опубликованных аргументов; самое серьёзное затронуло Unbalanced Group Theorem — его заменили новым шагом прувера. Задачи делили на 108 вех и ~380 подзадач; агенты брали issues в GitHub и отчитывались в Slack. Lean проверяет каждый шаг вывода; совпадение формальной формулировки с классификацией по-прежнему подтверждают люди... Источники: https://axiommath.ai/research/the-enormous-theorem-formalized/ https://the-agent-report.com/2026/10/axiom-cfsg-agent-swarm/ #AI #Математика #Lean #Axiom #Агенты