Классификацию конечных простых групп полностью формализовали в Lean
На странице проекта cfsg.axiommath.ai представлена полная формализация классификации конечных простых групп в системе Lean. Формализация следует доказательству первого поколения, и каждый логический шаг проверен ядром (kernel) Lean.
Сама классификация, как напоминают авторы страницы, одно из великих коллективных достижений математики. Её доказательство первого поколения занимает тысячи журнальных страниц, его писали около сотни математиков на протяжении нескольких десятилетий. Результат утверждает, что любая конечная простая группа либо циклическая простого порядка, либо знакопеременная, либо лиева типа, либо одна из 26 спорадических групп.
В ходе формализации команда обнаружила проблему в опубликованном аргументе для Unbalanced Group Theorem (теоремы о несбалансированных группах): нашлись контрпримеры к утверждению о замкнутости (closure assertion), которое используется в одном из опубликованных путей к этой теореме. Результат вынесен в отдельную статью: «Hexagon 2610.00575», 35 страниц. Статья объясняет возникшее препятствие и предлагает альтернативный аргумент для случая простых групп. Он построен на теории максимальных 2-компонент, созданной Соломоном в 1976 году; ключевой шаг, теорема 2.3 о сохранении простых «верхушек» (preservation of simple tops).
Авторы также пишут, что работают с теоретиками групп над сводом найденных в литературе ошибок (errata) и опубликуют его на этой же странице. Там же обещают новые статьи, выросшие из формализации. Полная история, по словам авторов, изложена в их блоге. В списке «Other contributors» на странице значатся, в частности, Ken Ono и Colin Defant, а также более двух десятков других участников.
Ключевые факты
- Опубликована полная формализация классификации конечных простых групп в Lean по доказательству первого поколения; каждый шаг проверен ядром Lean.
- Оригинальное доказательство занимает тысячи журнальных страниц и написано примерно сотней математиков за несколько десятилетий.
- При формализации найдены контрпримеры к утверждению о замкнутости, использованному в опубликованном пути к Unbalanced Group Theorem.
- Отдельная статья на 35 страниц (2610.00575) объясняет препятствие и даёт альтернативный аргумент для случая простых групп на основе теории максимальных 2-компонент Соломона 1976 года.
- Авторы собирают со специалистами по теории групп список найденных в литературе ошибок и обещают опубликовать его на странице.
Почему это важно
Классификация конечных простых групп, одно из крупнейших коллективных достижений математики, а её доказательство растянулось на тысячи журнальных страниц и десятилетия работы около сотни авторов. Проверить такой текст целиком вручную трудно, и полная формализация, в которой каждый шаг принимает ядро Lean, заменяет доверие к рассуждению машинной проверкой. Побочный результат, найденные при формализации контрпримеры к утверждению о замкнутости в опубликованном пути к Unbalanced Group Theorem и новый аргумент для случая простых групп.
Кому это важно
Прежде всего специалистам по теории конечных групп: команда собирает список найденных в литературе ошибок, а статья на 35 страниц даёт альтернативный путь к теореме. Также проект интересен тем, кто занимается формальной верификацией и системой Lean: это пример формализации огромного, написанного многими авторами математического доказательства.
Как это применить
На странице проекта можно по каждому утверждению прочитать формализованные формулировки (там есть режим «Zoom in to read each statement»). Статью о теореме о несбалансированных группах стоит читать по идентификатору 2610.00575. Свод ошибок в литературе и новые статьи авторы обещают добавлять на ту же страницу.
Можно ли доверять
Материал, это страница самого проекта, и все утверждения о результате исходят от его авторов. Корректность формализации опирается на проверку ядром Lean, но независимой оценки сообществом в тексте страницы нет. В тексте не указано, какой именно опубликованный путь к теореме содержал изъян, а подробности авторы выносят в блог и статью, которые в этом пересказе не разбирались. Утверждение о контрпримерах относится к конкретному утверждению о замкнутости; сама классификация под сомнение на странице не ставится.
Риски и подводные камни
Заявление о полноте формализации, слова авторов, независимых подтверждений страница не приводит. Нельзя считать, что найденная проблема ставит под сомнение саму классификацию: речь о контрпримерах к утверждению о замкнутости в одном из опубликованных путей к вспомогательной теореме, а авторы дают альтернативный аргумент для случая простых групп. Свод ошибок в литературе пока только готовится, и его содержание неизвестно.