Axiom: рои ИИ-агентов за 24 дня машинно проверили самое длинное доказательство в математике — классификацию конечных простых групп
Стартап опубликовал формализацию «огромной теоремы» в Lean объёмом около 43,1 млн строк и сообщил о 34 существенных отклонениях от опубликованной литературы. Независимо её пока никто не пересобрал.
ИИ-стартап Axiom заявляет, что создал первое полное компьютерно проверенное доказательство классификации конечных простых групп (CFSG) — результата, перечисляющего все «атомы» конечной симметрии. Исходное доказательство, написанное людьми, занимает около 15 000 страниц в более чем 500 статьях примерно 100 математиков.
Как это сделано
Согласно отчёту Axiom от 26 октября, инженеры и математики 24 дня (начиная с 1–2 октября 2026 года) управляли роями из десятков ИИ-агентов и получили около 43,1 млн строк кода в системе доказательств Lean, которая проверяет каждый логический шаг. Работа шла по доказательству «первого поколения», опиралась на Mathlib и была разбита на 108 этапов и около 380 задач. Среди прочего агенты доказали простоту группы Монстр.
Что нашли машины
Большинство проблем в литературе оказались мелкими (опечатки, ошибки в таблицах, пропущенные условия), но Axiom сообщает о 34 существенных отклонениях от опубликованного. Самое крупное касается теоремы о несбалансированных группах: агенты нашли контрпримеры к шагу в рассуждении Джона Уолтера 1986 года, и команда построила альтернативный путь, включая новый результат, доказанный её системой, — после консультаций с теоретиками групп Ричардом Лайонсом и Рональдом Соломоном. Axiom обещает опубликовать список опечаток и ошибок.
Оговорки
Lean проверяет выводы, но люди всё равно должны убедиться, что формальные формулировки и определения действительно выражают нужную теорему. По сообщениям СМИ на 27 октября, ни одна сторонняя группа ещё не пересобрала доказательство целиком; Axiom выложила репозиторий и артефакты сборки, чтобы это стало возможно. Утверждения приведены по отчёту самой компании.