Классификация конечных простых групп и проверка её доказательства (часть 1 из 3)

Как проверить доказательство, распределённое по сотням статей? Axiom Math объявила о первой полной формализации классификации конечных простых групп, CFSG, в Lean. По данным команды, за 24 дня десятки ИИ-агентов вместе с математиками и инженерами подготовили около 43,1 млн строк кода. Историческое доказательство занимает примерно 15 тысяч страниц в более чем 500 статьях около ста математиков. Lean проверяет выводы из точно записанных определений и гипотез.

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

Конечные группы разлагаются на неразложимые факторы, простые группы, в смысле теоремы Жордана и Гёльдера. CFSG перечисляет все возможные простые факторы.

Конечное поле представляет собой конечную систему чисел со сложением, вычитанием, умножением и делением на ненулевые элементы. Его размер определяет структуру с точностью до переобозначения; возможные размеры равны степеням простых чисел. Для групп размер такой однозначности не даёт.

Тем не менее CFSG даёт полный список простых групп. В него входят циклические группы простого порядка, то есть с простым числом элементов, знакопеременные группы чётных перестановок пяти и более символов, простые группы лиева типа над конечными полями с допустимыми параметрами, составляющие 16 бесконечных семейств, и 26 отдельных спорадических групп.

Крупнейшая спорадическая группа Monster имеет примерно 8 × 10⁵³ элементов. Главная трудность CFSG состоит в доказательстве полноты списка. Построить даже такую группу для этого недостаточно.

В 1954 году Брауэр предложил распознавать простые группы через инволюции и их централизаторы. Инволюция является нетождественной симметрией, двукратное применение которой возвращает исходное состояние. В её централизатор входят элементы, для которых умножение на неё слева и справа даёт один результат. В 1963 году Фейт и Томпсон доказали, что любая конечная простая группа с некоммутативным умножением имеет чётный порядок. По теореме Коши она содержит инволюцию. Поэтому стратегия применима ко всему этому классу. Их 255-страничное доказательство заняло целый выпуск журнала.