Axiom annuncia di aver verificato in Lean la classificazione dei gruppi finiti semplici, la dimostrazione più lunga della matematica

La start-up Axiom afferma di aver reso verificabile al computer la classificazione dei gruppi finiti semplici (spesso abbreviata CFSG), soprannominata « il teorema enorme »: una dimostrazione di circa 15.000 pagine, distribuita in più di 500 articoli scritti da un centinaio di matematici in diversi decenni. L’annuncio è arrivato su X questo martedì 27 ottobre alle 15:34, ora di Parigi, accompagnato da un lungo articolo del blog datato al giorno prima, da una mappa della dimostrazione interattiva e da un repository di codice.

Di cosa si parla

Un gruppo descrive delle simmetrie, come le 24 rotazioni che lasciano un cubo invariato. I gruppi finiti si decompongono in « mattoni » indivisibili, i gruppi semplici, un po’ come i numeri interi in numeri primi. La classificazione dice che l’elenco di questi mattoni è completo: gruppi ciclici di ordine primo, gruppi alterni (su almeno cinque elementi), sedici famiglie infinite di gruppi « di tipo di Lie » ed esattamente 26 gruppi sporadici, di cui il più grande, il gruppo Mostro. Questo risultato serve in molti campi (algebra, teoria dei numeri, combinatoria), ma pochissime persone possono verificarne l’insieme.

Axiom ha riscritto questa dimostrazione in Lean, un assistente di dimostrazione: un linguaggio in cui ogni definizione e ogni passo logico sono scritti con sufficiente precisione perché un programma li controlli. Il sito del progetto mostra 43,1 milioni di righe di Lean e 2,05 milioni di dichiarazioni.

Come sono stati messi a contributo gli agenti di IA

Il racconto di Axiom è soprattutto quello di un’organizzazione. Il progetto parte il 1° ottobre 2026 con una mappa della dimostrazione tratta dalla letteratura e dal codice Lean già esistente, suddivisa in 108 traguardi e circa 380 compiti. Già dal 2 ottobre, sciami di diverse decine di agenti AxiomProver, che utilizzano un mix mutevole di modelli, richiedono compiti tramite ticket GitHub e riferiscono su Slack. Agenti « capi » suddividono gli argomenti difficili e verificano gli enunciati; altri cercano risultati esistenti o scrivono le dimostrazioni.

Axiom non nasconde i fallimenti. Traguardi apparentemente semplici nascondevano enormi prerequisiti che gli agenti avevano supposto invece di dimostrare: decine di migliaia di righe sono state eliminate. Il tempo di ricompilazione è diventato anche un collo di bottiglia, risolto da un sistema di cache condiviso tra macchine. Gli umani restavano al centro: matematici per gli ostacoli di fondo, ingegneri per far funzionare il sistema.

Cosa ha trovato la macchina

Formalizzare obbliga a rendere esplicito ciò che un lettore umano completa da sé. Secondo Axiom, la maggior parte dei problemi rilevati era minore (refusi, tabelle errate, ipotesi dimenticate), ma 34 scostamenti notevoli con la letteratura hanno dovuto essere risolti. Il più serio tocca il teorema dei gruppi non bilanciati, nella versione di John Walter del 1986: gli agenti hanno trovato controesempi a una tappa del ragionamento, senza però confutare il teorema stesso. Con l’aiuto di Richard Lyons e Ronald Solomon, due specialisti storici della classificazione, è stata costruita un’altra strada a partire dai lavori di Solomon del 1976. Axiom la presenta come un nuovo risultato di teoria dei gruppi, descritto in un articolo che accompagna la pubblicazione.

Axiom promette di pubblicare la lista completa degli errata con un comitato di specialisti. Finché non è online, il numero totale di errori rilevati resta non verificabile.

I limiti da tenere a mente

Lean controlla le deduzioni, non il senso dell’enunciato: bisogna ancora che degli umani verifichino che il teorema finale e le sue definizioni dicano bene ciò che dice la classificazione. Axiom lo riconosce nel suo testo. Al momento in cui scriviamo, nessuna verifica indipendente completa è stata pubblicata e non abbiamo ricompilato noi stessi il repository. La formalizzazione non parte nemmeno da zero: integra circa 1,2 milioni di righe del progetto Qiuzhen-CFSG e si appoggia sulla libreria Mathlib.

Questo annuncio arriva il giorno dopo i risultati matematici rivendicati da OpenAI, che abbiamo presentato qui. L’approccio è diverso: OpenAI dice di aver trovato risultati nuovi, Axiom dice di aver verificato meccanicamente un risultato noto e di averne corretto dei pezzi.