Axiom Math, o companie din San Francisco care construiește sisteme AI pentru matematică, a lansat prima dovadă completă verificată de computer a Clasificării Grupurilor Finite Simple (CFSG), descrisă pe scară largă drept cea mai lungă dovadă din istoria matematicii. Potrivit anunțului companiei, inginerii și matematicienii au direcționat roiuri de zeci de agenți AI în doar 24 de zile pentru a produce aproximativ 43,1 milioane de linii de cod în asistentul Lean proof, verificând un rezultat care a cuprins anterior aproximativ 15.000 de pagini în peste 500 de articole de jurnal scrise de aproximativ 100 de matematicieni.
Realizarea aterizează într-un moment în care matematica asistată de mașini se accelerează rapid, iar agențiile de urmărire știri de cercetare AI au urmărit verificarea formală trecând de la o practică de nișă la o capacitate de frontieră. Ceea ce face această lansare neobișnuită este dimensiunea: formalizarea conține aproximativ 2,05 milioane de declarații organizate în 100 de etape, fiecare dintre ele verificată de kernel-ul Lean, micul nucleu de încredere care verifică fiecare pas logic.
Ce spune de fapt clasificarea
Grupurile simple finite sunt blocurile indivizibile ale simetriei finite, iar clasificarea - supranumită „teorema enormă” – oferă o listă completă a acestora. Conform documentației proiectului, fiecare grup finit simplu este unul din patru feluri: un grup ciclic de ordin prim, un grup alternant pe cel puțin cinci simboluri, una din șaisprezece familii infinite de grupuri de tip Lie construite pe câmpuri finite sau unul dintre exact 26 de grupuri sporadice care nu se încadrează în nicio familie.
Demonstrarea că această listă epuizează toate posibilitățile a fost nevoie de cea mai mare parte a unui secol de efort colectiv. John Thompson, a cărui activitate a fost esențială pentru clasificare, a primit medalia Fields în 1970 și premiul Abel în 2008. Dovada a fost atât de lungă și atât de distribuită între lucrări și generații de matematicieni, încât îndoielile persistente cu privire la completitudinea ei au persistat de zeci de ani - îndoieli că această formalizare le risipă acum oficial.
Roiuri de agenți din 500 de surse
Dovada originală este împrăștiată în peste 500 de articole și cărți, multe scrise cu decenii în urmă în notații incompatibile. Un inginer Axiom a descris metoda în discuția Hacker News despre lansare: un roi de agenți a fost însărcinat să parcurgă toate aceste surse, partea grea fiind asamblarea totul într-un întreg coerent, deoarece același concept informal poate fi formalizat în moduri ușor diferite, dar incompatibile din punct de vedere matematic.
Postarea pe blog a companiei afirmă că efortul a durat 24 de zile de la început până la lansare, inginerii umani și matematicienii conducând roiurile de agenți mai degrabă decât să lucreze linie cu linie. Rezultatul urmează etapele anterioare de auto-formalizare de profil înalt din 2026, inclusiv dovezi Lean ale teoremelor clasice majore produse cu modele de frontieră, dar la o scară nu s-a abordat niciun proiect anterior.
34 Abateri de la înregistrarea publicată
Traducerea dovezii publicate într-o formă care poate fi verificată de mașină a expus probleme reale în literatura matematică. Axiom raportează că majoritatea problemelor au fost minore - erori de tipar, greșeli în tabele sau ipoteze abandonate. Dar au existat 34 de abateri demne de remarcat de la înregistrarea publicată care trebuiau rezolvate înainte ca formalizarea să fie finalizată.
Cea mai substanțială a vizat Teorema Grupului Dezechilibrat. În timp ce a oficializat o rută de primă generație către rezultat, echipa a găsit contraexemple pentru o afirmație de încheiere folosită într-un argument publicat. În consultare cu teoreticienii grupului de experți, au construit o rută alternativă construită pe tehnicile structurale din epoca lui Daniel Gorenstein - în special teoria celor două componente maxime din anii 1970 - și au publicat soluția ca o nouă lucrare de teorie a grupului de 35 de pagini, postată ca preprint 2610.00575. Compania spune că va publica o listă lungă de errate în beneficiul comunității matematice, compilată în consultare cu teoreticienii grupului pe a căror activitate se bazează clasificarea.
De ce contează matematica verificată automat
Valoarea unei formalizări nu este doar că un computer a aprobat dovada. O formalizare Lean reduce baza de încredere la nucleul asistentului de probă – un program mic, puternic auditat – în loc de încrederea acumulată a mii de pagini citite de specialiști dispersați. Comentatorii de pe thread-ul Hacker News, unde povestea a atras sute de voturi pozitive, au remarcat că cunoașterea empirică a motivului pentru care este valabilă clasificarea riscă să dispară literalmente odată cu retragerea generației inițiale de matematicieni, pentru că nicio persoană nu putea ține întregul argument în cap.
Există ecouri practice și în alte părți în fizică. Cel mai mare dintre cele 26 de grupuri sporadice, grupul Monstru, apare în programul „monstruos moonshine” care conectează simetria finită la funcții modulare – lucru care i-a adus lui Richard Borcherds o medalie Fields în 1998 – și în propunerea lui Edward Witten din 2007 care leagă simetriile monstrului de entropia tridimensională simplificată a universului negru. O clasificare verificată pune matematica structurală de bază pe un teren mai ferm pentru exact aceste tipuri de aplicații interdisciplinare.
Ce urmează
Axiom spune că mai multe lucrări derivate din formalizare sunt pe drum, alături de proiectul errata. Pentru comunitatea de metode formale, versiunea stabilește un nou punct de referință pentru ceea ce proiectele de verificare direcționate de agent pot încerca; pentru matematică, transformă o realizare de colaborare întinsă, de o jumătate de secol, într-un singur artefact pe care orice computer îl poate verifica. Clasificarea nu mai este doar crezută. Este acum, în sensul cel mai literal, dovedit - și dovada este disponibilă pentru descărcare și verificare de oricine.
