[Перевод] Агенты Axiom Math доказали полноту классификации конечных простых групп всего лишь в 41,3 млн. строчках кода Lean

26 октября 2026 года компания Axiom Math сообщила о завершении полной формализации Теоремы о классификации простых конечных групп.

В международном математическом сообществе теорема известна как CFSG — Classification of Finite Simple Groups. Эта фундаментальная теорема перечисляет все строительные блоки, из которых состоят конечные простые математические группы.

Теорема утверждает, что

Любая конечная простая группа относится только к одному из четырех типов и никаких других типов конечных простых групп не существует.

Начиная с середины XX века над доказательством полноты этой классификации трудилось около ста математиков. В 1983 году Даниэль Горенштейн объявил о завершении работы. Позже выяснилось, что в доказательстве остались незаполненные части. В 2004 году они были дописаны и представлены в 1221 страничной монографии.

В текущем виде доказательство занимает более 15 тысяч страниц, разбросанных по более чем 500 статьям. За это теорему о классификацию прозвали Огромной теоремой.

Огромная теорема (Enormous theorem) — один из самых объемных результатов в истории математики. Ни один человек не способен удержать в голове все связи между положениями теоремы, поэтому формальная компьютерная проверка ее положения принципиально важна для развития математики.

Axiom Math использовала для формализации доказательства рой ИИ-агентов. На обработку массива информации и выводы они потратили 24 дня. За это время агенты сгенерировали 43,1 миллиона строк кода Lean, 2,05 миллиона математических утверждений, описали более 100 этапов доказательства и предоставили 715 ссылок. Также в ходе работы агенты нашли и исправили ошибки в статьях и вывели новые результаты теории групп.

Теперь математические рассуждения CFSG организованы в строгую верифицируемую формальную систему.

Конечные простые группы

Математическая группа — это алгебраическая структура, состоящая из множества и заданной на нем бинарной операции. Операция ассоциативна. Множество замкнуто относительно этой операции, то есть результат применения операции к любым двум элементам снова принадлежит исходному множеству. Во множестве существует нейтральный (единичный) элемент, и для каждого элемента множества существует обратный ему элемент.

Сами по себе группы служат для описания симметрий. Типичный пример — повороты куба, совмещающие его с самим собой. Всего есть 24 таких поворота, каждый из них — элемент множества поворотов и вместе они образуют группу.

Группа, состоящая из конечного числа элементов называется конечной. Сложные конечные группы могут быть разложены на более простые базовые части, подобно тому, как целые числа раскладываются на простые множители. Эти, далее неделимые базовые группы, называются простыми конечными группами (finite simple groups).

Основная теорема арифметики утверждает, что для целых чисел разложение на простые множители однозначно. Для групп cуществует теорема Жордана‑Гельдер, которая гарантирует однозначность состава простых групп, но не порядка их склейки.

Классификация конечный простых групп описывает характер каждой группы. Их полный перечень является для математиков аналогом периодической таблицы Менделеева.

Всего есть четыре типа конечный простых групп:

• циклические группы простых порядков,

• знакопеременные группы,

• 16 бесконечных семейств групп типа Ли,

• 26 спорадических группы.

Циклические группы — это простейший тип, который описывает одномерные симметрии, похожие на движение стрелок часов или вращение правильного многоугольника или многогранника.

Знакопеременные группы состоят из четных перестановок объектов. Их размер растет стремительно. Например, обычные перестановки колоды из 52 карт образуют группу из примерно 8×10⁶⁷ элементов.

Группы типа Ли — это матричные группы над конечными полями, объединенные в 16 бесконечных, но строго структурированных семейств.

Спорадические группы — вершина иерархии. Они состоят из 26 уникальных исключений, которые математически не вписываются ни в одно бесконечное семейство. Самая большая среди них — группа Монстр (Monster group). Она содержит около 8×1⁵³ элементов. Самая маленькая — группа Матье M₁₁ порядка 7 920.

Однако идентификация простых групп — лишь половина работы. Настоящая сложность заключается в доказательстве того, что помимо указанных типов не существует ни 27-й спорадической простой группы, ни какого‑либо нового, еще не открытого типа.

История доказательства

Исторически доказательство CFSG опиралось на стратегию Ричарда Брауэра (1954). Он предложил распознавать простые группы через изучение их инволюций — элементов порядка два. Дальнейшую базу заложили Уолтер Фейт и Джон Томпсон, доказав в 1963 году теорему о том, что всякая неабелева конечная простая группа имеет четный порядок и, следовательно, содержит инволюцию.

Теорема Фейта‑Томпсона (также известная как теорема о нечетном порядке) утверждает, что всякая конечная группа нечетного порядка разрешима, а значит не может быть простой и некоммутативной одновременно. Из этого следует, что все интересные простые группы некоммутативные и обязаны иметь четный порядок. Поэтому в их структуре обязательно есть инволюция — элемент порядка 2. Это сужает поиск и служит отправной точкой для анализа по инволюциям, который и ведет к классификации.

В 1972 году Дэниел Горенстейн изложил 16-шаговую программу завершения классификации, а в 1983 году объявил ее оконченной. Однако заявление оказалось преждевременным. Фрагмент, связанный с квазитонкими группами, опирался на незавершенную рукопись Джеффри Мейсона и был закрыт Майклом Ашбахером и Стивеном Смитом лишь в 2004 году. Так сформировалось доказательство первого поколения.

Квазитонкие группы (quasithin groups) — класс групп с особенно малым набором подгрупп определенного вида. Их разбор оказался самым трудным случаем всей классификации и потребовал отдельной монографии Ашбахера‑Смита объемом в 1221 страницу.

Несмотря на официальное завершение классификации в 2004 году, ни один человек физически не мог перепроверить цепочку рассуждений такого объема. Грандиозное доказательство напоминает сеть связей, охватывающую десятилетия. Теорема в одной статье ссылается на теорему из другой, которая, в свою очередь, опирается на леммы из еще более ранних работ. Многие шаги опускают условия, которые авторам кажутся очевидными. Даже если каждая отдельная статья выглядит разумной, одному человеку практически невозможно проверить каждое соединение во всей системе.

Из‑за колоссальной разрозненности литературы и нестыковок в нотациях математики взялись за доказательство второго поколения. К 2023 году вышло 10 томов из предполагаемых 12, но проект до сих пор не завершен.

Axiom Math ставила целью верифицировать полное доказательство первого поколения.

Агентная работа

1 октября 2026 года Axiom открыла канал в Slack и подготовила дорожную карту доказательства со 108 этапами и примерно 380 задачами, используя существующую библиотеку Lean и математическую литературу.

2 октября первая партия агентов начала брать задачи через GitHub Issues.

Агенты выполняли разные функции. Одни отвечали за разложение теорем, другие искали существующие результаты, третьи генерировали доказательства в Lean, четвертые проверяли утверждения и переписывали код. Люди решали ключевые вопросы и координировали непрерывную работу систему.

Вскоре после запуска проекта возникла проблема: агент мог доказать некоторое математическое утверждение, но не обязательно то, которое действительно нужно проекту.

Например, исходное требование состояло в том, чтобы доказать, что мост может безопасно пропускать тяжелые грузовики. Для этого агент сначала добавил условие о том, что опоры моста достаточно прочны, но не проверил его. С этим предположением он успешно доказал, что грузовик может проехать, и даже Lean признал всю цепочку вывода. Но проблема состояла в том, что достаточная прочность опор моста вообще не была доказана.

Подобные проблемы повторялись на ранней стадии. Некоторые кажущиеся завершенными математические доказательства незаметно вводили недоказанные предпосылки. Axiom пришлось удалить десятки тысяч строк кода, построенного на этих предположениях, и перезапустить работу.

Далее, по мере роста кодовой базы, скорость проверки Lean перестала поспевать за выводом агентов. Изменение базовой теоремы могло потребовать перепроверки всего зависящего от нее кода. Для решения вопроса инженеры внедрили общий кэш сборки и механизм параллельной проверки, позволяющий разным агентам максимально использовать подтвержденные результаты.

10 октября из Slack‑канала команды пришла новость о доказательстве простоты группы Монстра: «We proved Monster is simple».

Три дня спустя работа проекта внезапно замедлилась. 13 октября за весь день команда завершила лишь один этап доказательства. Проблема заключалась в том, что оставшиеся математические вопросы были слишком сложными — под одной большой задачей скрывалось множество нерешенных мелких. Хотя агенты могли продолжать писать новые доказательства, им было сложно оценить, сколько ключевых шагов уже решено и как далеко они от окончательной цели.

Axiom пришлось пересмотреть стратегию. Она разбила сложные доказательства на более мелкие и ясные задачи и требовала от агентов пояснять, как эти небольшие доказательства комбинируются для получения необходимого заключения.

Ошибки в доказательствах

Формализация в Lean вскрыла 34 серьезных расхождения с опубликованными статьями. Люди часто опускают знакомые им рассуждения, тогда как Lean требует явной записи каждой предпосылки. Поэтому в процессе формализации агенты обнаружили расхождения с литературой, включая опечатки, пропущенные условия и неполные выводы.

Самым критическим оказался пробел в доказательстве теоремы о несбалансированных группах (Unbalanced Group Theorem), опубликованным Джоном Уолтером в 1986 году.

UGT — важный инструмент классификации конечных простых групп. Она позволяет по конкретной локальной структуре группы судить о ее типе. Один из ее ключевых этапов по умолчанию предполагает, что после применения определенной операции к конкретному семейству групп, связанные простые группы по‑прежнему принадлежат исходному семейству. Агенты нашли контрпример. Он не опровергал вывод UGT, но означал, что при использовании этого доказательства один из шагов должен быть обоснован по другому.

Столкнувшись с ошибкой в доказательстве, ИИ самостоятельно построил альтернативный путь и вывел новое групповое свойство «сохранения простых топов» (Preservation of simple tops). Результат был опубликован в статье «The Unbalanced Group Theorem» как Теорема 2.3.

Вместе с другими результатами, статья завершила доказательство UGT, необходимое для классификации.

Итог — 41,3 миллиона строк кода Lean

В конечном итоге Axiom выложила весь проект на GitHub, сделав его общедоступными.

A Lean formalization of the Classification of Finite Simple Groups

Он содержит 41,3 миллиона строк кода Lean и не содержит sorry. Окончательный результат опирается только на стандартные аксиомы и может быть пошагово проверен.

В Lean ключевое слово sorry — это плейсхолдер, который позволяет утверждать любое предложение без необходимого доказательства. Если в проекте есть хоть одно sorry, формально он не доказан. Поэтому стандарт качества сообщества Lean гласит — «никаких извинений» («no sorry»).

Для наглядности Axiom создала интерактивный граф зависимостей между доказательствами. Он позволяет проследить, на какие теоремы опирается выбранный вывод.

Финальное предложение классификации гласит, что каждая конечная простая группа изоморфна некоторой группе, содержащейся в списке.

Значимость проделанной выходит далеко за рамки чистой алгебры.

Во‑первых, Axiom Math показала, что ИИ способен не просто решать отдельные олимпиадные задачи, а полноценно работать с гигантскими, распределенными во времени системами человеческих знаний: сводить воедино сотни статей, выстраивать между ними связи и находить пробелы, десятилетиями остававшиеся незамеченными.

Во‑вторых, разрозненный массив математических фактов превратился в строгое цифровое доказательство. Теперь любой математик может развернуть граф зависимостей CFSG вплоть до исходной аксиомы, проверить точные формулировки каждого промежуточного шага и использовать готовые модули Lean в новых исследованиях.

В‑третьих, величайшая теорема XX века наконец получила полное, логически выверенное доказательство.

Вопрос закрыт.

Рассказ команды:
https://axiommath.ai/research/the-enormous-theorem-formalized/