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

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

«Сегодня мы выпускаем первое полное доказательство классификации конечных простых групп (CFSG), проверенное компьютером», — написала компания в своём объявлении. Классификация определяет основные строительные блоки конечных групп. Первоначальное доказательство занимает около 15 000 страниц и изложено более чем в 500 статьях примерно 100 математиков; за такой масштаб оно получило прозвище «огромная теорема».

Что выпустила Axiom

CFSG устанавливает, что любая конечная простая группа является циклической группой простого порядка, знакопеременной группой на множестве как минимум из пяти элементов, одной из шестнадцати бесконечных семейств групп лиева типа, построенных над конечными полями, или одной из ровно 26 отдельных спорадических групп; в объявлении отмечается, что некоторые авторы считают группу Титса 27-й. Самая большая спорадическая группа — группа Монстр — была построена Робертом Гриссом в 1980 году с использованием алгебры размерности 196 884.

Работа математиков над доказательством растянулась на десятилетия. В 1963 году Уолтер Фейт и Джон Томпсон доказали, что порядок любой неабелевой конечной простой группы чётен. Их статья объёмом 255 страниц заняла целый выпуск Pacific Journal of Mathematics. В 1972 году Дэниел Горенстайн изложил программу из шестнадцати шагов для завершения классификации, а в 1983 году объявил её завершённой. Однако квазитонкий случай основывался на незаконченной рукописи Джеффри Мейсона, пока Майкл Ашбахер и Стивен Смит не опубликовали в 2004 году изложение объёмом 1 221 страницу, завершив тем самым то, что стало известно как доказательство первого поколения. Более систематическое доказательство второго поколения, начатое Горенстайном и Ричардом Лайонсом и позднее продолженное вместе с Рональдом Соломоном и Инной Капдебоск, остаётся незавершённым, поэтому Axiom формализовала доказательство первого поколения.

На странице проекта говорится, что формализация следует доказательству первого поколения и что каждый логический шаг проверяется ядром Lean; там также указаны 43,1 млн строк Lean, 2,05 млн объявлений и корпус из 715 статей и книг. По словам Axiom, карта доказательства опиралась на тома доказательства второго поколения, а формализация включает около 1,2 млн строк кода из более раннего проекта Qiuzhen-CFSG и построена на Mathlib, за разработку которой компания благодарит сотни участников. Среди ключевых участников проекта названы Дин Кьюретон, Василий Ильин, Бхавик Мехта и Нильс Фосс, а главным исследователем — Летун Хонг.

В общедоступном репозитории GitHub результат описан как доказательство на Lean4 без использования sorry, зафиксированное на версии 4.35.0-rc3, построенное на Mathlib и проекте TauCeti и использующее только стандартные аксиомы Classical.choice, propext и Quot.sound, без native_decide. Формулировка классификации в терминах формализации, взятая из TauCeti, гласит: «Любая конечная простая группа изоморфна одной из явно построенных групп, включённых в список классификации». В README сказано, что команда lake build проверяет всю разработку, а открытые изменения инструмента сборки Lake и оптимизации, которые команда планирует внести в основной проект, позволили сократить время сборки до менее чем 24 часов; код распространяется по лицензии Apache-2.0.

24 дня работы роя агентов

1 октября 2026 года Axiom открыла канал в Slack для координации проекта. Уже существовавшие наработки на Lean и внутренняя карта доказательства, составленная по опубликованной литературе, разделили работу на 108 этапов и около 380 более мелких задач. Первый рой приступил к работе 2 октября 2026 года: агенты брали этапы, создавая задачи в GitHub Issues, и отчитывались о выполненной работе в Slack. Ведущие агенты разбивали сложные рассуждения на части и проверяли формулировки, тогда как другие искали уже полученные результаты или писали доказательства на Lean. Агент мог поручить другим агентам найти недостающие предварительные результаты; полученные ими результаты попадали в общий репозиторий.

Первые успехи выявили слабые места. За некоторыми этапами, которые казались вполне посильными, скрывались огромные объёмы предварительных результатов, которые агенты считали само собой разумеющимися, вместо того чтобы доказывать их. Команда удалила десятки тысяч строк, основанных на этих предположениях, и начала заново, выбрав более надёжный план. Один из первых этапов касался теоремы о функторе-сигнализаторе; предполагаемое доказательство опиралось на структурные предположения, которые ещё требовалось обосновать. Узким местом стало и время сборки: агенты создавали доказательства быстрее, чем Lean успевал их перепроверять. По словам Axiom, инженеры компании распределили результаты кэшированных сборок между рабочими узлами, запускали независимые проверки параллельно и выносили затратные вычисления над конечными структурами в отдельные сертификаты, которые можно было проверять независимо. Компания утверждает, что эти изменения ускорили проверку на порядки.

10 октября 2026 года в сообщении канала объявили, что агенты доказали простоту группы Монстр, рассказывает компания. Агенты также формализовали существование группы Монстр с помощью алгебры Грисса и доказали теорему, отождествляющую группы типа Монстр с группой Монстр. 13 октября 2026 года удалось закрыть только один этап, и инженеры организовали пересмотр плана: незавершённые этапы разбили на более мелкие теоремы с точными формулировками. Для каждого разбиения требовалось показать, как из отдельных частей можно получить исходный этап с помощью короткого доказательства на Lean.

Пробелы, обнаруженные в опубликованном доказательстве

Как сообщает Axiom, перевод доказательства на Lean выявил проблемы в опубликованных аргументах. Большинство из них были незначительными — опечатки, ошибки в таблицах или пропущенные гипотезы, — однако компания насчитала 34 существенных расхождения с опубликованным текстом. Самое значительное из них связано с теоремой о несбалансированной группе (Unbalanced Group Theorem, UGT).

Один из примеров обнаружился в томах Асхбахера и Смита о квазитонких группах: одна из лемм утверждала равенство двух числовых величин. Агенты нашли контрпример с группой SL₂(5): одна величина в нём равнялась 1, тогда как из утверждавшегося равенства следовало, что она должна быть равна 2. Замена равенства на неравенство исправила лемму, но в дальнейших рассуждениях равенство использовалось для исключения случаев, поэтому команда расширила один из предыдущих аргументов, чтобы охватить эти конфигурации.

UGT позволяет определить всю группу по сведениям о её подгруппах: согласно аннотации сопроводительной статьи, при выполнении индуктивных гипотез классификации существование нетривиальной подгруппы нечётного порядка, нормальной в централизаторе инволюции, означает, что исходная простая группа имеет тип Ли в нечётной характеристике либо является знаковой группой одной из определённых степеней. Axiom подошла к UGT через монографию Джона Уолтера 1986 года и при формализации этого доказательства обнаружила явные контрпримеры к использовавшемуся в нём утверждению о замкнутости: операция, которая, как предполагалось, сохраняет соответствующие простые группы в заданном семействе, могла породить группу, прямо исключённую из этого семейства.

Согласно описанию компании, если начать с PSL₂(49), инволюция поля которой имеет централизатор PGL₂(7), то в результате операции получается простая компонента PSL₂(7). Она исключена из семейства, поскольку 7 — простое число Мерсенна. Axiom отмечает, что эти контрпримеры не опровергают саму UGT и даже не опровергают вывод предложения II.5.9(ii) Уолтера.

Исправление опиралось на теорию максимальных 2-компонент Соломона 1976 года, которая, по словам Axiom, легла в основу альтернативного доказательства, созданного и формализованного системой AxiomProver. Ключевой шаг, сформулированный в статье как теорема 2.3 (сохранение простых вершин), Axiom описывает как новый результат теории групп, доказанный AxiomProver. Вместе с редукциями Гилмана и Соломона и теоремами распознавания Фута и Харриса он даёт необходимую для классификации формулировку UGT для простых групп. После формализации математики Axiom нашли более короткий вывод, использующий методы первого поколения и изложенный в замечании 9.5: он приводит к тому же заключению без теоремы 2.3.

Эта статья, The Unbalanced Group Theorem, подготовленная Колином Дефантом и Кеном Оно, появилась на сервере препринтов Hexagon в версии 1 27 октября 2026 года по лицензии CC BY 4.0; на странице проекта указано, что в ней 35 страниц. Axiom сообщает, что работает с теоретиками групп над составлением списка опечаток и исправлений, обнаруженных в опубликованных работах, и разместит его на странице со списком исправлений проекта. Лайонс и Соломон, чьи работы лежат в основе классификации, участвовали в обсуждении исправления UGT. Компания также заявляет, что продолжит систематизировать и устранять ошибки и неточности при поддержке консультативного совета, в который входят Лайонс и Соломон, а также внешнего консультанта Дэна Накано. Axiom представляет свой вклад как создание возможности механически проверять доказательство, документирование обнаруженных препятствий и предоставление формализованных аргументов, устраняющих эти препятствия, одновременно подчёркивая, что классификация остаётся достижением математиков, открывших эти группы и разработавших соответствующие аргументы.