Самую длинную теорему математики теперь проверяет машина: ИИ-агенты собрали её на Lean за 24 дня

Раньше классификацию конечных простых групп держали на себе люди: больше 500 статей, около 100 математиков, первое сводное доказательство Ашбахера и Смита 2004 года на 1221 странице. Теперь её целиком проверяет сборка на Lean 4, и проверка укладывается в сутки.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Работу разбили на 108 вех и около 380 мелких задач, закрывали их рои из десятков агентов на меняющейся смеси моделей.

Что нашли по дороге. При переводе в Lean агенты поймали 34 значимых расхождения с публикациями: опечатки, ошибки в таблицах, потерянные гипотезы. В quasithin-томах Ашбахера и Смита оказалось ложное равенство, контрпримером к нему стала SL₂(5). Самый серьёзный пробел был в Unbalanced Group Theorem. Его закрыли новой теоремой 2.3 «Preservation of simple tops», опираясь на теорию максимальных 2-компонент Рональда Соломона 1976 года.

Посмотреть можно сейчас. Репозиторий AxiomMath/CFSG выложен под Apache 2.0: 43,1 млн строк Lean-кода и 2,05 млн деклараций, крупнейшая кодовая база на Lean. Собирается он командой lake build на Lean 4 v4.35.0-rc3 с Mathlib и TauCeti, код sorry-free и держится на трёх стандартных аксиомах Lean. Без установки Lean доказательство читается на cfsg.axiommath.ai, там же интерактивная карта зависимостей и список найденных ошибок литературы.

Формализация стоит и на чужом заделе: около 1,2 млн строк пришли из проекта Qiuzhen-CFSG, а формулировку теоремы Axiom взяла из TauCeti и её корректность оставляет на суд теоретиков групп. Сторонних оценок в релизе нет, проверить результат Axiom приглашает математиков и Lean-сообщество.

Дальше ход за теоретиками групп: формулировку теоремы и новую теорему 2.3 предстоит проверить людям.