Axiom Math випускає Lean-доведення класифікації груп обсягом 43,1 млн рядків

Axiom Math повідомила 27 жовтня 2026 року, що випускає, за її словами, перше повне доведення класифікації скінченних простих груп, перевірене комп’ютером. Його створили за 24 дні інженери й математики, які керували роєм із десятків агентів ШІ, що написали приблизно 43,1 мільйона рядків коду в асистенті доведень Lean.

«Сьогодні ми випускаємо перше повне доведення класифікації скінченних простих груп (CFSG), перевірене комп’ютером», — написала компанія у своєму оголошенні. Ця класифікація визначає базові будівельні блоки скінченних груп, а її первинне доведення охоплює приблизно 15 000 сторінок у понад 500 статтях близько 100 математиків. Такий масштаб приніс йому прізвисько «гігантська теорема».

Що випустила Axiom

CFSG встановлює, що кожна скінченна проста група є циклічною групою простого порядку, альтернаційною групою на множині щонайменше з п’яти елементів, належить до однієї з шістнадцяти нескінченних родин груп типу Лі, побудованих над скінченними полями, або є однією з рівно 26 окремих спорадичних груп. В оголошенні зазначено, що деякі автори зараховують групу Тітса до них як 27-му. Найбільшу спорадичну групу, Монстра, Роберт Ґрісс побудував 1980 року, використавши алгебру розмірності 196 884.

Робота над доведенням силами математиків тривала десятиліттями. 1963 року Волтер Файт і Джон Томпсон довели, що порядок кожної неабелевої скінченної простої групи є парним. Їхня стаття обсягом 255 сторінок заповнила цілий випуск Pacific Journal of Mathematics. 1972 року Деніел Ґоренстайн окреслив програму з шістнадцяти кроків для завершення класифікації, а 1983 року оголосив її завершеною. Однак квазітонкий випадок спирався на незавершений рукопис Джеффрі Мейсона, аж доки Майкл Ашбахер і Стівен Сміт не опублікували 2004 року працю обсягом 1 221 сторінка, завершивши те, що згодом назвали доведенням першого покоління. Систематичніше доведення другого покоління, розпочате Ґоренстайном і Річардом Лайонсом, до яких згодом долучилися Рональд Соломон та Інна Капсебоск, досі не завершене, тож Axiom формалізувала доведення першого покоління.

На сторінці проєкту формалізацію представлено як доведення, що відтворює доведення першого покоління, причому кожен логічний крок перевіряє ядро Lean. Там також указано, що корпус охоплює 43,1 мільйона рядків Lean, 2,05 мільйона декларацій і 715 статей та книжок. За словами Axiom, карта доведення спиралася на томи другого покоління, а формалізація містить приблизно 1,2 мільйона рядків коду з попереднього проєкту Qiuzhen-CFSG і базується на Mathlib, внесок у який, за оцінкою компанії, зробили сотні учасників. Серед основних учасників проєкту названо Діна К’юретона, Василія Іліна, Бгавіка Мегту та Нільса Восса, а головним дослідником є Летонг Гонг.

У загальнодоступному репозиторії GitHub результат описано як доведення Lean4 без конструкцій sorry, зафіксоване на версії 4.35.0-rc3, побудоване на Mathlib і проєкті TauCeti та таке, що використовує лише стандартні аксіоми Classical.choice, propext і Quot.sound, без native_decide. Формулювання класифікації, взяте з TauCeti, звучить так: «Кожна скінченна проста група ізоморфна одній із груп, явно побудованих у списку класифікації». У файлі README сказано, що команда lake build перевіряє всю розробку, а відкриті зміни до інструмента збирання Lake та оптимізації, які команда планує передати до основного проєкту, скоротили час збирання до менш ніж 24 годин. Код поширюється за ліцензією Apache-2.0.

Рой агентів: 24 дні роботи

1 жовтня 2026 року Axiom створила канал у Slack для координації проєкту. Наявні напрацювання з Lean та внутрішня карта доведення, складена за опублікованою літературою, поділили роботу на 108 етапів і приблизно 380 менших завдань. Перший рій розпочав роботу 2 жовтня 2026 року: агенти бралися за етапи через задачі GitHub, а про виконану роботу звітували у Slack. Провідні агенти розкладали складні доведення на частини та перевіряли твердження, тоді як інші шукали вже відомі результати або писали доведення в Lean. Агент міг доручити іншим агентам довести відсутні передумови, а їхні результати додавали до спільного репозиторію.

На ранньому етапі виявилися слабкі місця. У деяких, на перший погляд, посильних етапах ховалися величезні передумови, які агенти припускали, а не доводили. Команді довелося видалити десятки тисяч рядків, побудованих на таких припущеннях, і почати спочатку за надійнішим планом. Один із ранніх етапів стосувався теореми про функтор сигналізатора: запропоноване доведення спиралося на структурні припущення, які ще потрібно було обґрунтувати. Вузьким місцем також став час збирання: агенти створювали доведення швидше, ніж Lean встигав їх повторно перевіряти. За словами Axiom, інженери розподілили кешовані результати збирання між робочими вузлами, запустили незалежні перевірки паралельно та винесли ресурсомісткі скінченні обчислення в окремі сертифікати, які можна перевіряти незалежно. Компанія стверджує, що ці зміни прискорили перевірку на кілька порядків.

10 жовтня 2026 року в повідомленні на каналі оголосили, що агенти довели простоту Монстра, розповідає компанія. Агенти також формалізували існування Монстра через алгебру Ґрісса та теорему, яка ототожнює групи типу Монстра з Монстром. 13 жовтня 2026 року вдалося завершити лише один етап, і інженери організували перегляд плану: незавершені етапи розділили на менші, точно сформульовані теореми. Для кожного такого розбиття потрібно було коротким доведенням у Lean показати, як ці частини разом дають змогу завершити початковий етап.

Прогалини в опублікованому доведенні

Як повідомляє Axiom, перенесення доведення до Lean виявило проблеми в опублікованих аргументах. Більшість із них були незначними — друкарські помилки, помилки в таблицях або пропущені гіпотези, — але компанія нарахувала 34 суттєві розбіжності з опублікованим текстом; найзначніша з них стосувалася теореми про незбалансовану групу (Unbalanced Group Theorem, UGT).

Один із прикладів виявився в томах Ашбахера і Сміта про квазітонкі групи: в одній лемі стверджувалося, що два числові значення рівні. Агенти знайшли контрприклад із групою SL₂(5), у якому одне значення дорівнювало 1, тоді як заявлена рівність вимагала значення 2. Заміна рівності на нерівність виправила лему, однак у подальших аргументах рівність використовували, щоб виключити певні випадки, тож команда розширила попередній аргумент, аби охопити й ці конфігурації.

UGT допомагає визначити всю групу за інформацією про її підгрупи: згідно з анотацією супровідної статті, за індуктивних гіпотез класифікації наявність нетривіальної підгрупи непарного порядку, нормальної в централізаторі інволюції, означає, що вихідна проста група належить до груп типу Лі над полем непарної характеристики або є знакоперемінною групою певного степеня. Axiom підійшла до UGT через працю Джона Волтера 1986 року; формалізуючи цей аргумент, її агенти знайшли явні контрприклади до використаного в ньому твердження про замкненість: операція, яка, як вважалося, зберігає відповідні прості групи в певній родині, могла породити групу, прямо виключену з цієї родини.

За викладом компанії, якщо почати з PSL₂(49), інволюція поля якої має централізатор PGL₂(7), ця операція дає просту компоненту PSL₂(7), виключену з родини, оскільки 7 — просте число Мерсенна. Axiom зазначає, що ці контрприклади не спростовували саму UGT і навіть не заперечували висновку з твердження II.5.9(ii) Волтера.

Виправлення спиралося на теорію максимальних 2-компонентів Соломона 1976 року, яка, за словами Axiom, дала основні ідеї для альтернативного аргументу, створеного й формалізованого системою AxiomProver. Ключовий крок, сформульований у статті як теорема 2.3 (збереження простих верхів), Axiom описує як новий результат у теорії груп, доведений за допомогою AxiomProver; у поєднанні з редукціями Гілмана й Соломона та теоремами розпізнавання Фута й Гарріса він дає потрібне для класифікації формулювання UGT для простих груп. Після формалізації математики Axiom знайшли коротше виведення в межах методів першого покоління, зафіксоване в примітці 9.5, яке приводить до того самого висновку без теореми 2.3.

Ця стаття, The Unbalanced Group Theorem, написана Коліном Дефантом і Кеном Оно, з’явилася на сервері препринтів Hexagon у версії 1 27 жовтня 2026 року за ліцензією CC BY 4.0; на сторінці проєкту зазначено, що вона має 35 сторінок. Axiom повідомляє, що співпрацює з теоретиками груп над збиранням виправлень, виявлених у науковій літературі, і опублікує їх на сторінці зі списком виправлень проєкту. Лайонса й Соломона, чиї праці лежать в основі класифікації, залучили до консультацій щодо виправлення UGT; компанія повідомляє, що й надалі впорядковуватиме виправлення та працюватиме над їх усуненням разом із консультативною радою, до якої входять вони обоє, а також зовнішній радник Ден Накано. Axiom визначає свій внесок як створення можливості механічно перевірити доведення, документування виявлених перешкод і надання формалізованих аргументів для їх подолання, водночас наголошуючи, що класифікація залишається здобутком математиків, які відкрили ці групи й розробили відповідні аргументи.