Axiom Math publikuje 43,1 mln wierszy dowodu klasyfikacji grup w Lean

Axiom Math poinformowało 27 października 2026 r., że publikuje to, co określa jako pierwszy kompletny, sprawdzony komputerowo dowód twierdzenia o klasyfikacji skończonych grup prostych. Dowód powstał w ciągu 24 dni, gdy inżynierowie i matematycy kierowali zastępami kilkudziesięciu agentów AI, które napisały około 43,1 mln wierszy kodu w asystencie dowodzenia Lean.

„Dziś publikujemy pierwszy kompletny, sprawdzony komputerowo dowód twierdzenia o klasyfikacji skończonych grup prostych (CFSG)” — napisała firma w swoim ogłoszeniu. Klasyfikacja wskazuje podstawowe elementy składowe grup skończonych, a jej oryginalny dowód zajmuje około 15 000 stron w ponad 500 artykułach napisanych przez około 100 matematyków. Skala tego przedsięwzięcia przyniosła mu przydomek „ogromne twierdzenie”.

Co opublikowała Axiom

CFSG dowodzi, że każda skończona grupa prosta jest grupą cykliczną rzędu pierwszego, grupą alternującą działającą na co najmniej pięciu symbolach, należy do jednej z szesnastu nieskończonych rodzin grup typu Liego konstruowanych nad ciałami skończonymi albo jest jedną z dokładnie 26 izolowanych grup sporadycznych. W ogłoszeniu zaznaczono, że niektórzy autorzy zaliczają grupę Titsa jako 27. grupę. Największa grupa sporadyczna, grupa Monster, została skonstruowana przez Roberta Griessa w 1980 r. przy użyciu algebry o wymiarze 196 884.

Prace nad dowodem prowadzonym przez matematyków trwały dziesięciolecia. W 1963 r. Walter Feit i John Thompson udowodnili, że każda nieabelowa skończona grupa prosta ma parzysty rząd. Ich 255-stronicowy artykuł wypełnił cały numer czasopisma „Pacific Journal of Mathematics”. W 1972 r. Daniel Gorenstein przedstawił szesnastopunktowy program dokończenia klasyfikacji, a w 1983 r. ogłosił, że została ukończona. Przypadek grup kwazycienkich opierał się jednak na niedokończonym rękopisie Geoffreya Masona aż do 2004 r., kiedy Michael Aschbacher i Stephen Smith opublikowali opracowanie liczące 1221 stron, zamykając to, co stało się znane jako dowód pierwszej generacji. Bardziej systematyczny dowód drugiej generacji, nad którym prace rozpoczęli Gorenstein i Richard Lyons, a do którego później dołączyli Ronald Solomon i Inna Capdeboscq, pozostaje nieukończony. Z tego powodu Axiom sformalizowała dowód pierwszej generacji.

Na stronie projektu przedstawiono formalizację jako opartą na dowodzie pierwszej generacji, w której każdy krok logiczny sprawdza jądro Lean. Wymieniono tam 43,1 mln wierszy kodu Lean, 2,05 mln deklaracji oraz 715 artykułów i książek w korpusie. Axiom informuje, że mapa dowodu opierała się na tomach poświęconych dowodowi drugiej generacji, a formalizacja zawiera około 1,2 mln wierszy kodu z wcześniejszego projektu Qiuzhen-CFSG i korzysta z Mathlib, za którego rozwój firma dziękuje setkom współtwórców. Wśród głównych współtwórców projektu wymieniono Deana Curetona, Vasily’ego Ilina, Bhavika Mehtę i Nielsa Vossa, a funkcję głównego badacza pełni Letong Hong.

Publiczne repozytorium w serwisie GitHub opisuje wynik jako dowód w Lean4, który nie zawiera żadnych luk oznaczonych jako sorry i jest przypięty do wersji 4.35.0-rc3. Dowód zbudowano na Mathlib i projekcie TauCeti; wykorzystuje wyłącznie standardowe aksjomaty Classical.choice, propext i Quot.sound, bez native_decide. Formalne sformułowanie twierdzenia o klasyfikacji, zaczerpnięte z TauCeti, brzmi: „Każda skończona grupa prosta jest izomorficzna z jedną z jawnie skonstruowanych grup na liście klasyfikacyjnej”. W pliku README napisano, że polecenie lake build sprawdza cały projekt, a otwarte zmiany w narzędziu do budowania Lake i optymalizacje, które zespół planuje włączyć do projektu nadrzędnego, skróciły czas budowania do mniej niż 24 godzin. Kod jest objęty licencją Apache-2.0.

24-dniowa praca zespołu agentów

1 października 2026 r. Axiom utworzyła kanał w Slacku, aby koordynować projekt. Wcześniejsze prace w Lean oraz wewnętrzna mapa dowodu opracowana na podstawie opublikowanej literatury pozwoliły podzielić przedsięwzięcie na 108 kamieni milowych i około 380 mniejszych zadań. Pierwszy zespół agentów rozpoczął pracę 2 października 2026 r.; agenci przejmowali kamienie milowe za pośrednictwem zgłoszeń w GitHubie i informowali o ukończonych pracach na Slacku. Główni agenci rozkładali trudne argumenty na części i weryfikowali twierdzenia, a pozostali wyszukiwali istniejące wyniki lub pisali dowody w Lean. Agent mógł też zlecić innym agentom uzupełnienie brakujących przesłanek, a uzyskane wyniki trafiały do wspólnego repozytorium.

Wczesne postępy ujawniły słabe punkty. Niektóre pozornie łatwe do zrealizowania kamienie milowe kryły ogromne przesłanki, które agenci przyjęli bez dowodu. Zespół usunął dziesiątki tysięcy wierszy kodu opartych na tych założeniach, po czym rozpoczął pracę od nowa, stosując solidniejszy plan. Jedno z wczesnych zadań dotyczyło twierdzenia o funktorze sygnalizatora, którego kandydat na dowód opierał się na założeniach strukturalnych wymagających jeszcze uzasadnienia. Czas budowania również stał się wąskim gardłem, ponieważ agenci tworzyli dowody szybciej, niż Lean mógł je ponownie sprawdzać. Axiom informuje, że jej inżynierowie rozdzielali wyniki buforowanych kompilacji między pracowników, uruchamiali niezależne kontrole równolegle i przenosili kosztowne obliczenia skończone do osobnych, niezależnie sprawdzalnych certyfikatów. Według firmy te zmiany przyspieszyły weryfikację o kilka rzędów wielkości.

Jak relacjonuje firma, 10 października 2026 r. w kanale pojawiła się wiadomość, że agenci udowodnili, iż grupa Monster jest prosta. Agenci sformalizowali również istnienie grupy Monster za pomocą algebry Griessa oraz twierdzenie utożsamiające grupy typu Monster z grupą Monster. 13 października 2026 r. udało się zamknąć tylko jeden kamień milowy, więc inżynierowie zorganizowali ponowne planowanie prac i podzielili niedokończone kamienie milowe na mniejsze, precyzyjnie sformułowane twierdzenia. Każdy taki podział musiał pokazywać, w jaki sposób poszczególne części pozwolą zrealizować pierwotny kamień milowy za pomocą krótkiego dowodu w Lean.

Luki wykryte w opublikowanym dowodzie

Jak informuje Axiom, przekład dowodu na Lean ujawnił problemy w opublikowanych argumentach. Większość z nich była drobna — chodziło o błędy typograficzne, błędy w tabelach lub pominięte założenia — jednak firma odnotowała 34 istotne rozbieżności względem opublikowanego materiału. Najpoważniejsze dotyczyły twierdzenia o niezrównoważonej grupie (Unbalanced Group Theorem, UGT).

Jeden z przykładów pochodził z tomów Aschbachera i Smitha poświęconych grupom quasi-cienkim: w jednym z lematów stwierdzono równość dwóch wielkości liczbowych. Agenci znaleźli kontrprzykład dotyczący grupy SL₂(5), w którym jedna z tych wielkości wynosiła 1, podczas gdy z podanej równości wynikało, że powinna wynosić 2. Zastąpienie równości nierównością poprawiło lemat, ale w późniejszych argumentach równość wykorzystywano do wykluczania przypadków, więc zespół rozszerzył wcześniejszy argument, aby objąć nim te konfiguracje.

UGT pozwala rozpoznać całą grupę na podstawie informacji o jej podgrupach: zgodnie ze streszczeniem towarzyszącego artykułu, przy spełnieniu indukcyjnych założeń klasyfikacji istnienie nietrywialnej podgrupy rzędu nieparzystego, normalnej w centralizatorze inwolucji, wymusza, by rozpatrywana grupa prosta była grupą typu Liego nad ciałem o nieparzystej charakterystyce albo grupą alternującą określonych stopni. Axiom podjął się analizy UGT na podstawie monografii Johna Waltera z 1986 roku. Podczas formalizowania tego argumentu agenci firmy znaleźli jawne kontrprzykłady dla użytego w nim twierdzenia o domknięciu: operacja, która miała zachowywać powiązane grupy proste w obrębie określonej rodziny, mogła prowadzić do grupy wyraźnie z tej rodziny wykluczonej.

Według opisu firmy, wychodząc od PSL₂(49), którego inwolucja ciała ma centralizator PGL₂(7), otrzymuje się w wyniku tej operacji składową prostą PSL₂(7). Jest ona wykluczona z tej rodziny, ponieważ 7 jest liczbą pierwszą Mersenne’a. Axiom zaznacza, że kontrprzykłady nie obalały samego UGT ani nawet wniosku z twierdzenia II.5.9(ii) Waltera.

Naprawa opierała się na teorii maksymalnych 2-składowych Solomona z 1976 roku, która — jak podaje Axiom — dostarczyła kluczowych idei do alternatywnego argumentu opracowanego i sformalizowanego przez system AxiomProver. Kluczowy krok, przedstawiony w artykule jako twierdzenie 2.3 (zachowanie prostych wierzchołków), Axiom opisuje jako nowy wynik w teorii grup, dowiedziony przez AxiomProver. W połączeniu z redukcjami Gilmana i Solomona oraz twierdzeniami o rozpoznawaniu grup Foote’a i Harrisa pozwala on uzyskać postać UGT dotyczącą grup prostych, potrzebną do klasyfikacji. Po formalizacji matematycy z Axiom znaleźli krótsze wyprowadzenie, wykorzystujące metody pierwszej generacji i zapisane jako uwaga 9.5, które prowadzi do tego samego wniosku bez użycia twierdzenia 2.3.

Artykuł The Unbalanced Group Theorem, którego autorami są Colin Defant i Ken Ono, ukazał się w serwisie preprintów Hexagon jako wersja 1 dnia 27 października 2026 roku na licencji CC BY 4.0; na stronie projektu podano, że liczy 35 stron. Axiom informuje, że współpracuje z teoretykami grup, aby zebrać erraty znalezione w literaturze, i opublikuje je na stronie z erratami projektu. Lyons i Solomon, których prace stanowią podstawę klasyfikacji, konsultowali naprawę UGT. Firma zapowiada, że będzie nadal opracowywać erraty i usuwać wskazane w nich błędy we współpracy z radą doradczą, w której zasiadają Lyons i Solomon, a także z zewnętrznym doradcą Danem Nakano. Axiom przedstawia swój wkład jako umożliwienie mechanicznego sprawdzania dowodu, udokumentowanie napotkanych przeszkód oraz dostarczenie sformalizowanych argumentów, które je rozwiązują. Jednocześnie podkreśla, że klasyfikacja pozostaje osiągnięciem matematyków, którzy odkryli te grupy i opracowali dotyczące ich argumenty.