Axiom Math за 24 дня формализовала «Огромную теорему» в 43,1 млн строк Lean

Axiom Math объявила о завершении компьютерной проверки теоремы классификации конечных простых групп (CFSG), которую математики называют «Огромной теоремой». Десятки ИИ-агентов за 24 дня написали около 43,1 млн строк кода на Lean и формализовали доказательство, которое занимает 15 000 страниц в более чем 500 научных статьях. Над ним около 100 учёных работали десятилетиями. Axiom называет результат первым полным доказательством CFSG, которое можно проверить компьютером. Код и материалы выложены для независимого изучения.

Периодическая таблица симметрий

Самый простой способ понять, что классифицирует теорема, — куб. Его можно повернуть 24 способами так, чтобы он выглядел точно так же. Эти повороты образуют математическую группу. CFSG описывает фундаментальные «строительные блоки», из которых собраны все конечные группы симметрий. Получается своего рода периодическая таблица симметрий, которую используют в алгебре, теории чисел и математической физике.

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

Арифметика проекта: 43 миллиона строк за 24 дня

Цифры задают масштаб. 43,1 млн строк за 24 дня дают порядка 1,8 млн строк в сутки, или около 75 тысяч в час, если считать круглосуточно. На одну страницу бумажного доказательства приходится примерно 2 900 строк формального кода. Формализация на порядки подробнее исходного текста, потому что в статьях математики пропускают «очевидные» шаги, а Lean такого не позволяет.

Это агентная работа, а не одна длинная генерация. Десятки агентов вели параллельные ветки формализации, и итоговый код должен был сойтись в одно доказательство, которое принимает проверяющее ядро. Именно проверка ядром отличает такой результат от обычного вывода языковой модели: ошибочный шаг просто не пройдёт.

Что нашли агенты по ходу работы

Формализация дала не только подтверждение, но и новые находки. Axiom перечисляет такие результаты:

• около 43,1 млн строк кода на Lean, созданных за 24 дня десятками ИИ-агентов;
• 34 существенных расхождения с опубликованными математическими работами;
• контрпримеры к некоторым утверждениям из литературы и альтернативные доказательства для них;
• новый результат в теории групп, необходимый для выбранного пути доказательства;
• в отдельных случаях — найденные ошибки в исходных рассуждениях и новые математические аргументы, которые их исправляют;
• совместная работа с математиками, включая специалистов, участвовавших в первоначальной классификации.

Человеческое участие здесь существенно. Когда формализация упирается в расхождение с публикацией, нужен эксперт, который отличит опечатку от настоящей дыры. Опыт авторов исходной классификации помогал понять, где формальная версия должна следовать оригиналу, а где нужен другой путь.

Что из этого можно забрать в практику

Главный вывод для индустрии: агенты, которые пишут и самопроверяют код в среде с жёстким верификатором, способны справляться с задачами, непосильными для ручной работы. Lean выступает здесь судьёй, который не принимает на веру ни людей, ни модель. Та же схема применима к любой области, где результат можно проверить автоматически: верификация критичного ПО, протоколов, криптографических конструкций.

Есть и осторожное замечание. Компьютерная проверка гарантирует, что доказательство верно относительно записанных определений и формулировок. Поэтому открытый код важен не меньше самого результата: математики смогут прочитать определения и убедиться, что формализовано именно то, что нужно. Вопрос о цене такого прогона (затраты на вычисления и токены) Axiom в анонсе не приводит. Именно эта цифра покажет, станет ли формальная перепроверка фундаментальных результатов рутиной или останется разовым проектом.

Для математиков сигнал понятный. Литература, которую раньше приходилось принимать на доверии к авторитету, теперь поддаётся полной механической перепроверке, и на этом пути уже нашлись 34 существенных расхождения.