Axiom Math ha annunciato il completamento e la pubblicazione di una dimostrazione formalizzata del teorema di classificazione dei gruppi semplici finiti, realizzata attraverso un sistema coordinato di agenti di intelligenza artificiale e verificata mediante l’assistente di dimostrazione Lean. Il progetto, completato nell’arco dichiarato di 24 giorni, comprende circa 43,1 milioni di righe di codice Lean e 2,05 milioni di dichiarazioni formali, con un corpus di riferimento costituito da 715 libri e pubblicazioni scientifiche. La società presenta il risultato come la prima formalizzazione completa del teorema sottoposta alla verifica di un sistema automatico, utilizzando un insieme di agenti AI coordinati da ingegneri e matematici. Il lavoro riguarda uno dei più estesi risultati della matematica moderna, la cui dimostrazione tradizionale è distribuita su circa 15.000 pagine e oltre 500 pubblicazioni prodotte da un centinaio di ricercatori.
Il teorema identifica le possibili strutture dei gruppi semplici finiti, che rappresentano i componenti fondamentali utilizzati per descrivere la struttura dei gruppi finiti. La classificazione comprende i gruppi ciclici di ordine primo, i gruppi alterni su almeno cinque elementi, sedici famiglie infinite di gruppi di tipo Lie su campi finiti e 26 gruppi sporadici, con alcune convenzioni che considerano separatamente anche il gruppo di Tits. Tra i gruppi sporadici figura il Monster, costruito da Robert Griess nel 1980 attraverso un’algebra di dimensione 196.884. Lo sviluppo della dimostrazione matematica originale si è protratto per diversi decenni, comprendendo il risultato di Feit e Thompson del 1963 sui gruppi semplici non abeliani di ordine pari e il completamento del caso quasithin attraverso il lavoro di Michael Aschbacher e Stephen Smith pubblicato nel 2004. Axiom ha formalizzato la dimostrazione di prima generazione, mentre il programma di riorganizzazione della prova di seconda generazione rimane incompleto.
L’implementazione utilizza Lean 4, con il codice pubblico configurato per la versione 4.35.0-rc3, e si basa su Mathlib, TauCeti e contributi provenienti dal progetto Qiuzhen-CFSG, dei quali vengono riutilizzate circa 1,2 milioni di righe. La dimostrazione è descritta come priva di istruzioni sorry, utilizzate normalmente per rappresentare passaggi ancora non dimostrati, e impiega soltanto gli assiomi standard Classical.choice, propext e Quot.sound, senza ricorrere a native_decide. La proposizione formalizzata stabilisce che ogni gruppo semplice finito è isomorfo a uno dei gruppi esplicitamente costruiti nell’elenco della classificazione. La verifica avviene attraverso il kernel di Lean, che controlla i passaggi logici indipendentemente dal sistema che ha generato il codice. L’archivio pubblico è distribuito con licenza Apache 2.0 e può essere compilato attraverso il comando lake build, utilizzando le ottimizzazioni predisposte dal progetto.
La realizzazione ha richiesto un sistema di coordinamento tra numerosi agenti, organizzati attraverso GitHub e un canale Slack aperto il 1° ottobre 2026. Gli sviluppatori hanno inizialmente suddiviso il lavoro in 108 traguardi principali e circa 380 attività secondarie. Gli agenti responsabili dei diversi problemi potevano scomporre le dimostrazioni, ricercare risultati precedenti, generare codice Lean e delegare la verifica di prerequisiti ad altri agenti, integrando successivamente i risultati nel repository condiviso. Le prime attività hanno evidenziato problemi di dipendenze logiche non adeguatamente dimostrate, costringendo il gruppo a eliminare decine di migliaia di righe e riorganizzare le dimostrazioni. La verifica del codice ha rappresentato inoltre un limite computazionale, affrontato attraverso la distribuzione dei risultati di compilazione memorizzati nella cache, controlli paralleli e certificati verificabili separatamente per i calcoli più onerosi.
Tra i risultati intermedi figurano le formalizzazioni relative all’esistenza e alla semplicità del gruppo Monster, comunicate durante le attività del 10 ottobre. Nei giorni successivi il progetto ha attraversato ulteriori fasi di riorganizzazione, necessarie a trasformare obiettivi matematici troppo ampi in lemmi e teoremi più piccoli, collegati mediante dimostrazioni verificabili. Le ottimizzazioni dell’infrastruttura hanno successivamente portato il tempo di compilazione complessiva al di sotto delle 24 ore, secondo i dati pubblicati da Axiom. La disponibilità del codice consente alla comunità matematica e informatica di esaminare le definizioni, verificare le dipendenze e riprodurre i controlli utilizzando l’implementazione Lean, distinguendo il risultato formalmente verificabile dalle affermazioni sulle modalità e sui tempi della sua produzione.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI).