Часть 2 из 3

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

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

В аргументе Уолтера 1986 года предполагалось, что определённая операция сохраняет некоторое семейство простых групп. Контрпример использует группы PSL₂(q) и PGL₂(q), построенные из матриц 2 × 2 над полем с q элементами. Группа PSL₂(49) входит в семейство. Нетождественная симметрия поля из 49 элементов, которая сохраняет арифметику и при двукратном применении возвращает каждый элемент на место, задаёт полевую инволюцию группы. Это автоморфизм, то есть взаимно однозначное преобразование группы в себя, сохраняющее умножение, а не элемент самой группы. Неподвижные при нём элементы образуют централизатор PGL₂(7). На следующем шаге из централизатора выделяют простую подгруппу PSL₂(7). Она исключена из семейства, поскольку 7 = 2³ − 1 является простым числом Мерсенна. Значит, операция вывела нас за пределы семейства. Контрпример опровергает утверждение о замкнутости, но не UGT и не заключение соответствующего предложения Уолтера.

Смена доказательства UGT могла потребовать большого объёма новой формализации. После консультаций с Лайонсом и Соломоном AxiomProver построил альтернативный аргумент на основе теории Соломона 1976 года. В сопровождающей статье об UGT команда представляет новую теорему 2.3. При специальных гипотезах этого этапа CFSG сравнения подгрупп через связывающие их инволюции сохраняют соответствующую простую группу. Вместе с редукциями Гилмана и Соломона и теоремами распознавания Фута и Харриса это даёт нужную форму UGT для простых групп. Позднее математики Axiom нашли в рамках первого поколения более короткий путь без теоремы 2.3. Длинный путь оставили как формализованный аргумент, дающий дополнительный результат.

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