Axiom Math pubblica una dimostrazione Lean della classificazione dei gruppi, composta da 43,1 milioni di righe

Il 27 ottobre 2026 Axiom Math ha dichiarato di pubblicare quella che definisce la prima dimostrazione completa della classificazione dei gruppi semplici finiti verificata da un computer. Realizzata in 24 giorni da ingegneri e matematici che hanno coordinato decine di squadre di agenti IA, la dimostrazione è stata scritta nell’assistente di prove Lean e comprende circa 43,1 milioni di righe di codice.

«Oggi pubblichiamo la prima dimostrazione completa della classificazione dei gruppi semplici finiti (CFSG) verificata da un computer», ha scritto l’azienda nel proprio annuncio. La classificazione individua gli elementi costitutivi fondamentali dei gruppi finiti. La dimostrazione originale si estende per circa 15.000 pagine, distribuite in oltre 500 articoli scritti da circa 100 matematici: una portata che le è valsa il soprannome di teorema enorme.

Che cosa ha pubblicato Axiom

La CFSG stabilisce che ogni gruppo semplice finito è ciclico di ordine primo, alternante su almeno cinque simboli, appartiene a una delle sedici famiglie infinite di gruppi di tipo Lie costruiti su campi finiti oppure è uno dei 26 gruppi sporadici isolati; l’annuncio osserva che alcuni autori considerano il gruppo di Tits un ventisettesimo gruppo. Il più grande gruppo sporadico, il Mostro, fu costruito da Robert Griess nel 1980 usando un’algebra di dimensione 196.884.

Il lavoro umano sulla dimostrazione si è protratto per decenni. Nel 1963 Walter Feit e John Thompson dimostrarono che ogni gruppo semplice finito non abeliano ha ordine pari, in un articolo di 255 pagine che occupò un intero fascicolo del Pacific Journal of Mathematics. Nel 1972 Daniel Gorenstein delineò un programma in sedici passaggi per completare la classificazione e nel 1983 ne dichiarò conclusa la dimostrazione; tuttavia, il caso quasi-sottile si basava su un manoscritto incompiuto di Geoffrey Mason, finché nel 2004 Michael Aschbacher e Stephen Smith non pubblicarono un’analisi di 1.221 pagine, portando a termine quella che divenne nota come dimostrazione di prima generazione. Una dimostrazione di seconda generazione, più sistematica, avviata da Gorenstein e Richard Lyons e a cui si sono poi uniti Ronald Solomon e Inna Capdeboscq, è ancora incompleta; per questo Axiom ha formalizzato la dimostrazione di prima generazione.

La pagina del progetto spiega che la formalizzazione segue la dimostrazione di prima generazione, con ogni passaggio logico verificato dal kernel di Lean, e riporta 43,1 milioni di righe di Lean, 2,05 milioni di dichiarazioni e un corpus di 715 articoli e libri. Axiom afferma che la propria mappa della dimostrazione si è basata sui volumi della seconda generazione e che la formalizzazione incorpora circa 1,2 milioni di righe di codice del precedente progetto Qiuzhen-CFSG. Si basa inoltre su Mathlib, che l’azienda attribuisce al contributo di centinaia di persone. Il progetto indica Dean Cureton, Vasily Ilin, Bhavik Mehta e Niels Voss come collaboratori principali e Letong Hong come responsabile della ricerca.

Il repository pubblico su GitHub descrive il risultato come una dimostrazione in Lean4 priva di «sorry», fissata alla versione 4.35.0-rc3, basata su Mathlib e sul progetto TauCeti e che usa soltanto gli assiomi standard Classical.choice, propext e Quot.sound, senza native_decide. L’enunciato formale della classificazione, ripreso da TauCeti, recita: «Ogni gruppo semplice finito è isomorfo a uno dei gruppi costruiti esplicitamente nell’elenco della classificazione». Il README spiega che lake build verifica l’intero sviluppo e che le modifiche aperte allo strumento di compilazione Lake e le ottimizzazioni che il team intende integrare nel progetto principale hanno ridotto i tempi di compilazione a meno di 24 ore. Il codice è distribuito con licenza Apache-2.0.

Una squadra di agenti al lavoro per 24 giorni

Il 1° ottobre 2026 Axiom ha aperto un canale Slack per coordinare il progetto. Il lavoro già svolto in Lean e una mappa interna della dimostrazione, compilata a partire dalla letteratura pubblicata, hanno suddiviso l’impresa in 108 traguardi e circa 380 attività più piccole. La prima squadra di agenti è entrata in funzione il 2 ottobre 2026: gli agenti si assegnavano i traguardi tramite issue di GitHub e comunicavano su Slack le attività completate. Gli agenti responsabili scomponevano gli argomenti più difficili e verificavano gli enunciati, mentre gli altri cercavano risultati già esistenti o scrivevano dimostrazioni in Lean; ciascun agente poteva delegare ad altri agenti la ricerca dei prerequisiti mancanti, i cui risultati confluivano in un repository condiviso.

I primi progressi hanno messo in luce alcuni punti deboli. Alcuni traguardi, che sembravano gestibili, nascondevano prerequisiti enormi che gli agenti avevano dato per scontati invece di dimostrarli. Prima di ripartire con un piano più solido, il team ha cancellato decine di migliaia di righe basate su tali supposizioni; uno dei primi traguardi riguardava il teorema del funtore segnalatore, la cui dimostrazione candidata si basava su ipotesi strutturali ancora da giustificare. Anche i tempi di compilazione sono diventati un collo di bottiglia, perché gli agenti producevano dimostrazioni più rapidamente di quanto Lean riuscisse a verificarle di nuovo. Axiom afferma che i suoi ingegneri hanno distribuito tra i nodi di calcolo i risultati memorizzati nella cache, eseguito verifiche indipendenti in parallelo e spostato all’esterno i costosi calcoli finiti, producendo certificati verificabili separatamente. Secondo l’azienda, queste modifiche hanno accelerato la verifica di diversi ordini di grandezza.

Il 10 ottobre 2026 un messaggio nel canale annunciò che gli agenti avevano dimostrato che il Mostro è semplice, racconta l’azienda. Gli agenti hanno anche formalizzato l’esistenza del Mostro tramite l’algebra di Griess e un teorema che identifica con il Mostro i gruppi di tipo Mostro. Il 13 ottobre 2026 è stato completato un solo traguardo e gli ingegneri hanno avviato una riorganizzazione del lavoro, suddividendo i traguardi incompiuti in teoremi più piccoli, formulati con precisione. Per ogni scomposizione era necessario dimostrare, con una breve prova in Lean, come le singole parti consentissero di raggiungere il traguardo originario.

Lacune individuate nella dimostrazione pubblicata

La traduzione della dimostrazione in Lean ha messo in luce problemi negli argomenti pubblicati, riferisce Axiom. La maggior parte era di poco conto — errori tipografici, errori nelle tabelle o ipotesi omesse — ma l’azienda conta 34 discrepanze degne di nota rispetto a quanto pubblicato; la più sostanziale riguarda l’Unbalanced Group Theorem, o UGT.

Un esempio proviene dai volumi di Aschbacher e Smith sui gruppi quasi-sottili, in cui un lemma affermava l’uguaglianza tra due quantità numeriche. Gli agenti hanno trovato un controesempio relativo al gruppo SL₂(5), nel quale una quantità era pari a 1, mentre l’uguaglianza affermata richiedeva che fosse pari a 2. Sostituire l’uguaglianza con una disuguaglianza ha corretto il lemma, ma argomenti successivi si erano basati sull’uguaglianza per escludere alcuni casi; il team ha quindi ampliato un argomento precedente per includere quelle configurazioni.

L’UGT aiuta a identificare un intero gruppo a partire da informazioni sui suoi sottogruppi: secondo l’abstract di l’articolo che accompagna il lavoro, date le ipotesi induttive della classificazione, l’esistenza di un sottogruppo non banale di ordine dispari, normale nel centralizzatore di un’involuzione, implica che il gruppo semplice considerato sia di tipo di Lie in caratteristica dispari oppure alterno di determinati gradi. Axiom ha affrontato l’UGT partendo dalla monografia di John Walter del 1986 e, nel formalizzare quell’argomento, i suoi agenti hanno trovato controesempi espliciti a un’asserzione di chiusura in esso utilizzata: un’operazione che, secondo l’ipotesi, avrebbe dovuto mantenere i gruppi semplici associati all’interno di una famiglia specificata poteva produrre un gruppo esplicitamente escluso da essa.

Secondo quanto riferisce l’azienda, partendo da PSL₂(49), la cui involuzione di campo ha come centralizzatore PGL₂(7), l’operazione produce la componente semplice PSL₂(7), esclusa dalla famiglia perché 7 è un primo di Mersenne. Axiom osserva che i controesempi non confutavano l’UGT, né tantomeno la conclusione della Proposizione II.5.9(ii) di Walter.

La correzione si è basata sulla teoria delle 2-componenti massimali di Solomon del 1976, che, secondo Axiom, ha fornito le idee centrali per un argomento alternativo elaborato e formalizzato dal sistema AxiomProver. Il passaggio chiave, enunciato nell’articolo come Teorema 2.3 (preservazione delle sommità semplici), è descritto da Axiom come un nuovo risultato di teoria dei gruppi dimostrato da AxiomProver; insieme alle riduzioni di Gilman e Solomon e ai teoremi di riconoscimento di Foote e Harris, fornisce la formulazione dell’UGT per i gruppi semplici necessaria alla classificazione. Dopo la formalizzazione, i matematici di Axiom hanno trovato una dimostrazione più breve, basata sui metodi della prima generazione e riportata come Osservazione 9.5, che giunge alla stessa conclusione senza ricorrere al Teorema 2.3.

L’articolo, The Unbalanced Group Theorem, a cui hanno contribuito Colin Defant e Ken Ono, è apparso sul server di preprint Hexagon in versione 1 il 27 ottobre 2026, con licenza CC BY 4.0; la pagina del progetto lo indica come un testo di 35 pagine. Axiom afferma di collaborare con esperti di teoria dei gruppi per raccogliere le errata riscontrate nella letteratura e che le pubblicherà nella pagina delle errata del progetto. Lyons e Solomon, il cui lavoro è alla base della classificazione, sono stati consultati per la correzione dell’UGT; l’azienda afferma che continuerà a raccogliere e risolvere le errata con l’aiuto di un comitato consultivo che li comprende, insieme al consulente esterno Dan Nakano. Axiom presenta il proprio contributo come un modo per rendere la dimostrazione verificabile meccanicamente, documentare gli ostacoli incontrati e fornire argomenti formalizzati per superarli, precisando al contempo che la classificazione resta un risultato dei matematici che hanno scoperto i gruppi e sviluppato gli argomenti.