Классификация конечных простых групп (CFSG) в современной математике является одним из наиболее масштабных проектов доказательства.
Это доказательство, выполненное сотнями математиков в течение нескольких десятилетий, разбросано по сотням статей и монографий, общий объем которых приближается к двадцати тысячам страниц, что далеко превосходит возможности полной проверки одним человеком или даже отдельной командой.
В этом контексте внедрение ИИ для помощи в крупномасштабной формальной верификации становится новым путем, который необходимо попробовать.
Для продвижения развития ИИ для математики, по инициативе господина Шинтуна Яу, исследовательская команда, состоящая из студентов ведущего класса Института Цючжэнь Университета Цинхуа, а также Центра математических наук Яу, Института исследований интеллектуальной промышленности и Университета Уорика, предложила FormaTheoria — рабочий процесс искусственного интеллекта для помощи в математических исследованиях: позволить ИИ, исходя из оригинальной математической литературы, автоматически выявлять зависимости, интегрировать систему знаний, строить формальные доказательства и, наконец, передавать их помощнику доказательства Lean для пошаговой проверки.
По состоянию на август 2026 года FormaTheoria уже завершила формализацию четырех ключевых теорем на Lean, произведя более 994 тысяч строк взаимосвязанного кодоизированного математического знания. Хотя до полной верификации классификации конечных простых групп еще далеко, этот результат уже стал важной вехой на пути к этой конечной цели.
CFSG обеспечивает фундаментальную систему для множества важных математических результатов
«Классификация конечных простых групп» звучит весьма абстрактно. Проще говоря, она подобна «основному списку деталей» о конечной симметрии: любую сложную конечную симметричную структуру можно разложить на слои, в итоге получив набор базовых неделимых единиц; а роль CFSG — рассказать математикам, что именно представляют собой эти базовые единицы.
Обычно математическое исследование сначала разбивает сложную проблему на эти базовые единицы, а затем обрабатывает их по одному, опираясь на полный список, предоставленный CFSG. Таким образом, CFSG становится инфраструктурой, к которой могут обращаться другие доказательства. Если в этой «инфраструктуре» скрываются уязвимости, то многие последующие результаты, построенные на связанных с ней выводах, могут оказаться под угрозой.
Некоторые профессиональные обзоры предоставляют количественное доказательство применения GFSG. Американское математическое общество в 2018 году специально опубликовало монографию Стивена Д. Смита "Applying the Classification of Finite Simple Groups: A User’s Guide", объемом 231 страницу, 10 глав, в которой систематизированы сценарии применения GFSG. Открытый оглавление последних двух глав книги перечисляет 14 тематических приложений с номерами, включая дистанционно-транзитивные графы, гипотезу Фробениуса, алгоритмы групп перестановок, рост подгрупп конечно порожденных групп, расширения полей, накрытия римановых поверхностей, проблему Варинга в теории групп, экспандеры и приближенные группы и т.д.
Ценность применения GFSG также получила признание на самом высоком уровне международного математического сообщества. На Международном конгрессе математиков 2014 года Роберт Гуралник, лауреат премии Коула по алгебре Американского математического общества 2018 года, был приглашен выступить с пленарным докладом на тему "Applications of the Classification of Finite Simple Groups".
Эти приложения включают в себя крайне влиятельные академические результаты. CFSG является ключевым звеном в полной цепи доказательств ограниченной проблемы Бернсайда, за решение которой Ефим Зельманов получил Филдсовскую премию в 1994 году. Монография Смита также относит проблему Варинга на конечных простых группах и экспандеры к важным направлениям применения CFSG; соответствующие репрезентативные статьи были опубликованы в «Annals of Mathematics» (проблема Варинга; диаметры конечных простых групп и их приложения). Эти примеры показывают, что CFSG уже поддержала серию важных работ, получивших высшие академические награды и опубликованных в ведущих математических журналах.
В этом смысле CFSG уже стала многократно используемой базовой системой. По мере накопления результатов «ниже по течению» проверка ее корректности и воспроизводимости становится все более критичной. Осуществление машиночитаемой, отслеживаемой и повторяемой верификации CFSG приобретает значение, выходящее за рамки самой теории групп.
Однако трудность заключается в том, что доказательства этой базовой системы происходят из литературы разных эпох, разных авторов, используют разные обозначения, определения и условия по умолчанию, и одна ссылка может указывать на целый другой свод литературы. Исторически, важный пробел в доказательстве классификации был заполнен лишь спустя более двадцати лет двухтомной монографией объемом 1220 страниц. FormaTheoria должна не только пошагово проверять логические рассуждения, но и проверять, могут ли определения, условия и ссылки из сотен статей полностью соединиться, в конечном итоге формируя непрерывную цепь доказательств.
Как ИИ продвигает сверхмасштабные проекты доказательств
Многие системы ИИ для математики сталкиваются с уже подготовленной задачей, где все условия, определения и инструменты готовы, а ИИ только ищет доказательство. Но FormaTheoria другая: ей сначала нужно восстановить математическую основу задачи из разрозненной литературы, а затем завершить доказательство. Эта работа в основном сталкивается с четырьмя трудностями:
Во-первых, система заранее не знает, сколько материалов нужно изучить.
Одна ссылка может привести к другой статье, а та, в свою очередь, — к большему количеству предварительных работ. Изначально у проекта было только 3 основных источника, в процессе доказательства было обнаружено еще 12; позже добавленные материалы составили 65.6% от общего количества просмотренных страниц. Метод FormaTheoria таков: как только обнаруживается отсутствие необходимой предварительной теоремы, текущее доказательство приостанавливается, находится и формализуется эта зависимость, а затем возобновляется выполнение исходной задачи. Уже проверенные результаты сохраняются в единой базе знаний для многократного использования в последующих доказательствах.
Во-вторых, разные источники трудно напрямую соединить.
Разные авторы используют разные определения, обозначения и условия по умолчанию. Два определения могут быть математически полностью эквивалентными, но как только они записываются в код Lean, они могут оказаться несовместимыми. FormaTheoria будет неоднократно сравнивать оригинал и существующий код, строя необходимые отношения преобразования. Одновременно система защищает уже проверенные математические утверждения и проверяет, повлияет ли каждое исправление на последующие доказательства. Таким образом, несколько независимых книг и статей могут постепенно интегрироваться в одну теоретическую структуру.
В-третьих, код может пройти проверку, но при этом неверно интерпретировать оригинал.
Lean отвечает только за проверку логической согласованности доказательства и того, следует ли вывод из предпосылок, но не может оценить, насколько этот вывод верен по отношению к оригиналу. ИИ может упустить какое-то условие, спутать «все» и «существует» или даже ошибочно изменить вывод. Для этого в FormaTheoria специально установлен независимый контрольный этап: компонент перевода сначала записывает утверждение на Lean, а затем компонент проверки сверяет его с оригиналом по пунктам. Из 14 проанализированных в статье разделов литературы, перевод в первом раунде для 11 разделов был возвращен на доработку. Этот механизм независимой проверки стал, таким образом, вторым «страховочным уровнем» помимо машинной верификации.
В-четвертых, в самой оригинальной литературе также могут быть проблемы.
В старой литературе могут встречаться опечатки, отсутствующие условия или неоднозначные формулировки. FormaTheoria сохраняет оригинальные страницы и возвращается к ним для проверки, когда в последующем доказательстве возникает противоречие. Если литература поддерживает исправление, система добавляет условие или устанавливает отношение совместимости; если доказательств недостаточно, система записывает проблему и передает ее математикам-специалистам для оценки.
Помимо этого, этот проект требует от ИИ сохранять ритм в течение длительного периода. Один диалог не может вместить полную задачу. Для этого FormaTheoria использует постоянно обновляемую «карту доказательств» для управления прогрессом: более сложные цели разбиваются на меньшие вспомогательные теоремы, успешные результаты постепенно возвращаются к главной теореме, неудачные маршруты также записываются, чтобы система не попадала в один и тот же тупик снова и снова.
В стратегии параллельной работы проект также имеет особый дизайн. Взаимно независимые задачи могут выполняться одновременно; если несколько задач сталкиваются с одним и тем же предварительным результатом, система выполняет его только один раз и позволяет другим задачам повторно использовать его. А те общие математические содержания, которые могут затронуть все, изменяются последовательно, по одному, чтобы избежать конфликтов. Контрольные эксперименты в статье показывают, что этот подход к параллельной работе с учетом зависимостей дал ускорение в 4.2 раза на тестовых задачах.
Таким образом, FormaTheoria формирует полную рабочую цепочку: поиск литературы, дополнение зависимостей, перевод оригинала, построение доказательства, машинная верификация, независимая проверка, координация конфликтов и передача неясных вопросов математикам-специалистам. Каждый шаг имеет четкую ответственность и подкреплен доказательствами. Именно такой дизайн, ориентированный на реальные трудности, возникающие в сверхмасштабных проектах доказательств, позволяет ИИ постепенно связывать разрозненную математическую литературу в проверяемую, отслеживаемую и устойчиво расширяемую теоретическую систему.
△
Семь месяцев, четыре ключевые теоремы, почти миллион строк проверяемого кода
22 января 2026 года FormaTheoria впервые отправила код; к 2 августа 2026 года проект уже прошел ключевую теоретическую цепочку, ведущую к теореме Бендера–Судзуки, попутно завершив доказательства теоремы Фейта–Томпсона о группах нечетного порядка, теоремы Глаубермана Z* и теоремы Брауэра–Судзуки.
Эти четыре теоремы не изолированы друг от друга; они образуют важную, взаимосвязанную линию в классификации конечных простых групп, где доказательство каждой последующей теоремы часто опирается на обширный математический фундамент, заложенный предыдущими.
Снимок проекта по завершении этих доказательств включает:
- Более 994 тысяч строк кода на Lean;
- Более 850 файлов с кодом;
- Система изучила 15 книг и статей, всего 1037 страниц, из которых около двух третей были постепенно обнаружены в ходе продвижения доказательства.
Конечно, количество строк кода показывает лишь один аспект масштаба проекта. Если проследить назад от теоремы Бендера–Судзуки как конечной точки, проект уже сформировал сеть доказательств, содержащую 30298 математических утверждений и 186187 зависимостей, при этом самая длинная цепочка зависимостей достигает 458 уровней. Если включить соответствующий контент из базовой библиотеки Lean, эта сеть расширится до 74922 утверждений и более 1.44 миллиона зависимостей. Можно сказать, что за почти миллионом строк кода стоит запутанная, тесно связанная сеть доказательств. Это исследование показывает, что агенты ИИ уже могут, при совместном действии машинной верификации и многоуровневой проверки, непрерывно продвигать крупные, сверхдлинные математические проекты.
Фактический процесс выполнения проекта также характеризуется сверхдлинными циклами. Зафиксированный в статье самый длинный запуск агента ИИ длился 9.17 дней, в течение которых система выполнила 606 сжатий и реорганизаций накопленной информации, при этом постоянно сохраняя текущую цель доказательства, уже завершенные результаты и остающиеся нерешенные проблемы. Эти данные показывают, что система управляет постоянно эволюционирующей сверхдлинной сетью доказательств, которую невозможно охватить единичной генерацией или одним диалогом.
Раньше крупномасштабная математическая формализация в высокой степени зависела от ручного труда, обычно требующего совместной работы нескольких исследователей в течение нескольких лет. Историческая точка для сравнения: предыдущая формализация теоремы Фейта–Томпсона в Rocq была завершена примерно 15 людьми за шесть лет. А FormaTheoria завершила весь этот ручной проект за семь месяцев и продвинулась дальше, выполнив формализацию других ключевых теорем. Семь месяцев для одной задачи агента ИИ по-прежнему крайне длительный цикл выполнения, но по сравнению с традиционной ручной формализацией, вмешательство ИИ значительно сократило временные рамки проекта.
△
Формализация позволяет выявлять скрытые проблемы в литературе
Математическая литература обычно ориентирована на исследователей, знакомых с областью. Поэтому авторы часто опускают условия, уже появившиеся ранее, или предполагают, что читатель сможет распознать эквивалентность между разными определениями. Небольшие опечатки или ошибки в обозначениях при чтении человеком часто естественным образом игнорируются или исправляются. Но подход FormaTheoria иной: при переводе литературы построчно в код Lean каждое определение, каждое условие и каждый шаг рассуждения должны быть записаны ясно и недвусмысленно. Именно это строгое требование поточной проверки делает проблемы, скрытые в оригинальной литературе, очевидными.
В статье подробно описаны различные проблемы с литературой, обнаруженные в ходе проекта, включая несовместимые определения одного и того же понятия в разных источниках, пропущенные необходимые условия в формулировках теорем, неправильное расположение условий делимости и даже ошибки в индексах в доказательствах. Часть этих проблем может быть автоматически исправлена на основе контекста литературы; проблемы с недостаточными доказательствами передаются математикам для дальнейшей оценки.
Типичный пример взят из двух источников по теореме о группах нечетного порядка. В обоих источниках определена «максимальная подгруппа типа I», но различие в следующем: в одном требуется, чтобы некоторое свойство выполнялось для «каждой комплементарной структуры»; в другом требуется только, чтобы «существовала комплементарная структура», удовлетворяющая этому свойству. Формально первое, очевидно, сильнее второго, поэтому две системы определений не могут быть напрямую соединены. FormaTheoria в процессе формализации точно определила это различие, а затем, используя теорему Шура–Цассенхауза, доказала, что здесь два определения фактически эквивалентны, успешно построив мост между двумя источниками.
Другой пример взят из одной леммы Питерфальви. В формальной формулировке этой леммы было пропущено предварительное условие «порядок некоторой группы нечетен», однако последующее доказательство фактически зависело от этого условия. Хотя при применении этой леммы далее в тексте это условие уже гарантировалось предыдущим контекстом, и общая аргументация не прерывалась, Lean не будет автоматически добавлять этот фоновый слой информации. FormaTheoria, отследив путь доказательства и места использования этой леммы, автоматически добавила пропущенное условие в формулировку теоремы, сделав всю формализованную цепочку более полной и надежной.
△
Проект также обнаружил более прямые ошибки в литературе. В одном определении объект, который должен был быть H, был записан как M, причем две ссылки сохранили одну и ту же ошибку. В одной теореме Хупперта множитель d был помещен в неправильное условие делимости; система, найдя контрпример, остановила доказательство и передала вопрос математикам для проверки. Правильное условие было подтверждено вручную. В одном доказательстве Хигмана нумерация набора базисных векторов была записана от u0 до um, тогда как правильный диапазон должен был быть до um−1; эта ошибка индекса была автоматически обнаружена и исправлена системой в процессе доказательства.
Эти случаи отражают другую важную ценность машинной верификации для крупных математических проектов. FormaTheoria, строя формализованные доказательства, одновременно проводит детальную проверку оригинальной литературы: она записывает, где возникает проблема, какие условия требуются для последующего доказательства, на основе каких источников сделано исправление и повлияет ли исправление на другие результаты. Для CFSG, состоящей из сотен взаимосвязанных источников, такой отслеживаемый механизм проверки может преобразовать детали, которые раньше зависели от опыта читателя для восполнения, в четко проверяемые математические основания.
Перспективы на будущее
FormaTheoria пока не завершила полную формализацию классификации конечных простых групп, до конечной цели еще долгий путь. Проект ускоряется, неуклонно продвигаясь к полной формализации одного из самых масштабных проектов доказательств в современной математике. Существующие результаты показывают, что ИИ уже способен в течение нескольких месяцев поддерживать и расширять крупномасштабную математическую среду, отслеживать сложные зависимости между многочисленными источниками и строить взаимосвязанные, значительные по объему теоретические системы при строгой проверке. Границы возможностей ИИ, таким образом, начинают расширяться от решения изолированных математических задач до участия в систематическом построении математического знания.
Эта работа также создаст устойчиво расширяемую, многократно используемую математическую инфраструктуру. Традиционная литература может только сказать читателю «где написано доказательство»; формализованный код дополнительно записывает «от чего зависит каждый вывод», «как соединяются разные источники», «какие проблемы были исправлены» и организует проверенные определения, леммы и доказательства в модули знаний, доступные для прямого использования в последующих исследованиях. В будущем, после добавления инструментов объяснения, поиска и визуализации, эта сеть знаний может помочь исследователям быстрее понять общую структуру CFSG, повторно использовать существующие результаты и даже предоставить мощную поддержку математикам-людям в исследовании новых связей и открытии новых теорем.
Команда проекта FormaTheoria надеется исследовать модель взаимодействия человека и машины для эпохи ИИ: человек отвечает за определение достойных исследования проблем и принятие ключевых решений, ИИ берет на себя крупномасштабный поиск и вывод, а формальная система гарантирует, что каждый принятый шаг может быть перепроверен. Когда доказательство становится настолько огромным, что любой человек с трудом может его заново проверить, объединение этих трех элементов, возможно, станет совершенно новым путем для человечества в управлении сверхмасштабным математическим знанием.
Примечание: Состояние проекта и количественные результаты в статье соответствуют снимку на момент завершения в августе 2026 года.
Статья: https://arxiv.org/abs/2608.10894
Код: https://github.com/Qiuzhen-CFSG/CFSG
Эта статья из официального аккаунта WeChat "Квантовый бит", автор: команда FormaTheoria
