Axiom Math lansează o demonstrație Lean de 43,1 milioane de linii pentru clasificarea grupurilor

Axiom Math a anunțat pe 27 octombrie 2026 că publică ceea ce numește prima demonstrație completă, verificată de calculator, a Clasificării grupurilor finite simple. Aceasta a fost realizată în 24 de zile de ingineri și matematicieni care au coordonat roiuri de zeci de agenți IA, aceștia scriind aproximativ 43,1 milioane de linii de cod în asistentul de demonstrații Lean.

„Astăzi publicăm prima demonstrație completă, verificată de calculator, a Clasificării grupurilor finite simple (CFSG)”, a scris compania în anunțul său. Clasificarea identifică elementele fundamentale din care sunt alcătuite grupurile finite, iar demonstrația originală se întinde pe aproximativ 15.000 de pagini, în peste 500 de articole semnate de circa 100 de matematicieni. Amploarea sa i-a adus porecla de teoremă enormă.

Ce a lansat Axiom

CFSG stabilește că orice grup finit simplu este ciclic de ordin prim, alternant pe cel puțin cinci simboluri, face parte din una dintre cele șaisprezece familii infinite de grupuri de tip Lie construite peste corpuri finite sau este unul dintre cele exact 26 de grupuri sporadice izolate; anunțul menționează că unii autori numără grupul Tits drept al 27-lea. Cel mai mare grup sporadic, Monster, a fost construit de Robert Griess în 1980, folosind o algebră de dimensiune 196.884.

Demonstrația realizată de matematicieni s-a desfășurat de-a lungul mai multor decenii. În 1963, Walter Feit și John Thompson au demonstrat că orice grup finit simplu neabelian are ordin par, într-un articol de 255 de pagini care a umplut un număr întreg al revistei Pacific Journal of Mathematics. În 1972, Daniel Gorenstein a schițat un program în șaisprezece pași pentru finalizarea clasificării, iar în 1983 a declarat-o completă. Totuși, cazul quasithin se baza pe un manuscris neterminat al lui Geoffrey Mason până când Michael Aschbacher și Stephen Smith au publicat, în 2004, o tratare de 1.221 de pagini, încheind ceea ce a ajuns să fie cunoscut drept demonstrația de primă generație. O demonstrație de a doua generație, mai sistematică, începută de Gorenstein și Richard Lyons, cărora li s-au alăturat ulterior Ronald Solomon și Inna Capdeboscq, este încă incompletă, așa că Axiom a formalizat demonstrația de primă generație.

Pagina proiectului prezintă formalizarea ca urmând demonstrația de primă generație, fiecare pas logic fiind verificat de nucleul Lean, și menționează că aceasta cuprinde 43,1 milioane de linii Lean, 2,05 milioane de declarații și un corpus de 715 articole și cărți. Axiom afirmă că harta demonstrației s-a bazat pe volumele celei de a doua generații și că formalizarea încorporează aproximativ 1,2 milioane de linii de cod din proiectul anterior Qiuzhen-CFSG și se bazează pe Mathlib, la care, potrivit companiei, au contribuit sute de persoane. Proiectul îi menționează pe Dean Cureton, Vasily Ilin, Bhavik Mehta și Niels Voss drept colaboratori principali, iar pe Letong Hong drept investigator principal.

Depozitul public de pe GitHub descrie rezultatul drept o demonstrație Lean4 fără „sorry”, fixată la versiunea 4.35.0-rc3, construită pe Mathlib și proiectul TauCeti și folosind doar axiomele standard Classical.choice, propext și Quot.sound, fără native_decide. Enunțul formal al clasificării, preluat din TauCeti, este: „Orice grup finit simplu este izomorf cu unul dintre grupurile construite explicit în lista clasificării.” README-ul precizează că lake build verifică întreaga dezvoltare și că modificările aduse instrumentului de compilare Lake, împreună cu optimizările pe care echipa intenționează să le integreze în proiectul din amonte, au redus timpul de compilare la mai puțin de 24 de ore; codul este distribuit sub licența Apache-2.0.

Un efort colectiv de 24 de zile

Pe 1 octombrie 2026, Axiom a deschis un canal Slack pentru coordonarea proiectului. Lucrările Lean deja existente și o hartă internă a demonstrației, alcătuită pe baza literaturii publicate, au împărțit efortul în 108 etape și aproximativ 380 de sarcini mai mici; primul roi de agenți a devenit operațional pe 2 octombrie 2026, agenții revendicând etape prin probleme GitHub și raportând în Slack sarcinile finalizate. Agenții principali au descompus argumentele dificile și au verificat enunțurile, în timp ce alți agenți au căutat rezultate existente sau au scris demonstrații în Lean; un agent putea, de asemenea, să delege altor agenți identificarea premiselor lipsă, iar rezultatele acestora erau adăugate într-un depozit comun.

Progresele inițiale au scos la iveală puncte slabe. Unele etape care păreau ușor de gestionat ascundeau premise enorme pe care agenții le presupuseseră, în loc să le demonstreze, iar echipa a șters zeci de mii de linii construite pe aceste presupuneri înainte de a relua lucrul pe o bază mai solidă; o etapă timpurie privea teorema functorului de semnalizator, a cărei demonstrație propusă se baza pe ipoteze structurale care încă trebuiau justificate. Timpul de compilare a devenit, de asemenea, un obstacol, deoarece agenții produceau demonstrații mai repede decât le putea reverifica Lean. Axiom afirmă că inginerii săi au distribuit rezultatele compilărilor stocate în cache între mai multe mașini, au rulat verificări independente în paralel și au mutat calculele finite costisitoare în certificate care puteau fi verificate separat; compania spune că aceste schimbări au accelerat verificarea de mai multe ordine de mărime.

Pe 10 octombrie 2026, un mesaj de pe canal a anunțat că agenții demonstraseră că Monster este simplu, relatează compania; agenții au formalizat și existența lui Monster prin algebra Griess, precum și o teoremă care identifică grupurile de tip Monster cu Monster. Pe 13 octombrie 2026, a fost încheiată o singură etapă, iar inginerii au organizat o replanificare, împărțind etapele neterminate în teoreme mai mici, formulate cu precizie. Fiecare descompunere trebuia să arate cum puteau fi folosite componentele pentru a demonstra etapa inițială printr-o scurtă demonstrație Lean.

Lacune descoperite în demonstrația publicată

Traducerea demonstrației în Lean a scos la iveală probleme în argumentele publicate, relatează Axiom. Cele mai multe erau minore — greșeli de tipar, erori în tabele sau ipoteze omise — însă compania consemnează 34 de abateri semnificative față de materialele publicate, dintre care cea mai importantă privește Teorema grupului neechilibrat, sau UGT.

Un exemplu provine din volumele cvasi-subțiri ale lui Aschbacher și Smith, în care o lemă afirma că două mărimi numerice erau egale. Agenții au găsit un contraexemplu care implică grupul SL₂(5), în care una dintre mărimi era 1, deși egalitatea afirmată impunea valoarea 2. Înlocuirea egalității cu o inegalitate a corectat lema, dar argumentele ulterioare folosiseră egalitatea pentru a exclude anumite cazuri, așa că echipa a extins un argument anterior pentru a acoperi acele configurații.

UGT ajută la identificarea unui grup întreg pe baza informațiilor despre subgrupurile sale: potrivit rezumatului din articolul care însoțește lucrarea, în condițiile ipotezelor inductive ale clasificării, existența unui subgrup netrivial de ordin impar, normal în centralizatorul unei involuții, impune ca grupul simplu ambiant să fie de tip Lie în caracteristică impară sau alternant de anumite grade. Axiom a abordat UGT pornind de la monografia lui John Walter din 1986, iar în timp ce formalizau acel argument, agenții săi au găsit contraexemple explicite la o afirmație de închidere pe care acesta o folosea: o operație despre care se presupunea că păstrează grupurile simple asociate într-o anumită familie putea produce un grup exclus explicit din acea familie.

Potrivit relatării companiei, pornind de la PSL₂(49), a cărui involuție de corp are drept centralizator PGL₂(7), operația produce componenta simplă PSL₂(7), care este exclusă din familie deoarece 7 este un număr prim Mersenne. Axiom precizează că aceste contraexemple nu infirmau UGT și nici măcar concluzia Propoziției II.5.9(ii) a lui Walter.

Corectarea s-a bazat pe teoria componentelor 2 maximale a lui Solomon din 1976, care, potrivit Axiom, a furnizat ideile centrale pentru un argument alternativ produs și formalizat de sistemul său AxiomProver. Pasul-cheie, enunțat în articol ca Teorema 2.3 (păstrarea vârfurilor simple), este descris de Axiom drept un rezultat nou în teoria grupurilor, demonstrat de AxiomProver; împreună cu reducerile lui Gilman și Solomon și teoremele de recunoaștere ale lui Foote și Harris, acesta oferă forma UGT pentru grupurile simple, necesară clasificării. După formalizare, matematicienii Axiom au găsit o deducție mai scurtă, folosind metode de primă generație și consemnată în Remarca 9.5, care ajunge la aceeași concluzie fără Teorema 2.3.

Articolul, The Unbalanced Group Theorem, la care au contribuit Colin Defant și Ken Ono, a apărut pe serverul de preprinturi Hexagon în versiunea 1, la 27 octombrie 2026, sub licența CC BY 4.0; pagina proiectului îl indică drept o lucrare de 35 de pagini. Axiom spune că lucrează cu specialiști în teoria grupurilor pentru a centraliza eratele identificate în literatura de specialitate și că le va publica pe pagina de erate a proiectului. Lyons și Solomon, ale căror lucrări stau la baza clasificării, au fost consultați cu privire la corectarea UGT, iar compania spune că va continua să centralizeze și să soluționeze eratele împreună cu un consiliu consultativ din care fac parte și aceștia, alături de consilierul extern Dan Nakano. Axiom își descrie contribuția ca pe un efort de a face demonstrația verificabilă mecanic, de a documenta obstacolele întâmpinate și de a furniza argumente formalizate care le soluționează, precizând totodată că clasificarea rămâne realizarea matematicienilor care au descoperit grupurile și au dezvoltat argumentele.