Axiom Math полностью формализовала доказательство теоремы о классификации конечных простых групп

26 октября 2026 года компания Axiom Math сообщила о завершении полной формализации в Lean теоремы о классификации конечных простых групп, известной в мировом научном сообществе как Classification of Finite Simple Groups (CFSG).

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

Теорема CFSG утверждает, что любая конечная простая группа относится к одному из четырех типов:

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

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

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

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

Доказательство, над которым десятилетиями трудились около ста ученых, занимало более 15 тысяч страниц, разбросанных по сотням публикаций. За это классификацию прозвали "огромной теоремой". На то, чтобы перевести весь этот массив в машиночитаемый код, у роя ИИ-агентов ушло всего 24 дня.

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

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

Простая группа выступает своего рода "атомом" в алгебре групп: ее нельзя разложить на меньшие составляющие, подобно тому как простое число нельзя разложить на множители. Поскольку любая конечная группа симметрий собирается из простых, их полный перечень стал для математиков аналогом периодической таблицы Менделеева.

Четыре класса простых групп, составляющих таблицу, устроены совершенно по-разному.

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

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

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

Спорадические группы — вершина иерархии. Они состоят из 26 уникальных "островных" исключений, которые математически не вписываются ни в одно бесконечное семейство. Самая большая среди них — группа Монстр (Monster) — содержит около 8?10^{53} элементов.

Первые пять спорадических групп открыл Эмиль Матье в 1860-70-х годах. А группа Монстр, обнаруженный в 1980 году, стал последним кусочком мозаики.

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

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

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

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

Несмотря на официальное завершение классификации в 2004 году, ни один человек физически не мог перепроверить цепочку рассуждений такого объема.

Формализация в Lean вскрыла 34 серьезных логических расхождения с печатными источниками. Самым критическим оказался пробел в доказательстве теоремы о несбалансированных группах (Unbalanced Group Theorem) 1986 года. Столкнувшись с ошибкой в человеческом доказательстве, ИИ самостоятельно построил альтернативный путь и вывел новое групповое свойство "сохранения простых топов" (Preservation of simple tops), заполнив сорокалетний пробел в науке.

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

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

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

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

Ссылки на сайт проекта, рассказ команды о работе, код Lean и суперскую карту доказательства будут даны в комментариях.

Телеграм: t.me/ainewsline

Источник: vk.com

Комментарии: