Gli agenti di Axiom formalizzano in Lean la classificazione dei gruppi semplici finiti

Axiom Math ha detto il 26 ottobre 2026 di aver pubblicato la prima prova completa, verificata da un computer, della classificazione dei gruppi semplici finiti, scritta nell'assistente di dimostrazione Lean [1]. In 24 giorni, i suoi ingegneri e matematici hanno diretto sciami di dozzine di agenti di IA che hanno prodotto circa 43.1 milioni di righe di codice Lean [1][2].

Che cosa ha formalizzato Axiom?

La classificazione, spesso chiamata il teorema enorme, elenca i mattoni di tutti i gruppi finiti, la matematica della simmetria [1]. Dice che ogni gruppo semplice finito è ciclico di ordine primo, alterno, di tipo di Lie, o uno di 26 gruppi sporadici [2].

Axiom dice che la dimostrazione originale arriva a circa 15,000 pagine in più di 500 articoli di circa 100 matematici [1]. La versione Lean segue la dimostrazione di prima generazione e, secondo la pagina GitHub del progetto, è sorry-free, cioè nessun passo è lasciato senza prova [3].

Axiom dice che i suoi agenti di IA hanno prodotto circa 43.1 milioni di righe di Lean in 24 giorni. Il sito del progetto elenca 2.05 milioni di dichiarazioni e 715 articoli e libri nel corpus [2]. Axiom dice che la formalizzazione incorpora circa 1.2 milioni di righe da un progetto precedente, Qiuzhen-CFSG, e si basa sulla libreria Mathlib [1].

Come ha lavorato lo sciame di agenti?

Axiom ha aperto un canale Slack per il progetto l'1 ottobre 2026 e il primo sciame è andato in linea il 2 ottobre [1]. Una mappa della prova tratta dalla letteratura ha diviso il lavoro in 108 tappe e circa 380 compiti più piccoli, che gli agenti prendevano tramite issue di GitHub [1].

Gli agenti guida scomponevano gli argomenti difficili e rivedevano gli enunciati, mentre altri cercavano risultati già noti o scrivevano dimostrazioni in Lean [1]. Matematici umani affrontavano gli ostacoli matematici e gli ingegneri tenevano in funzione il sistema [1]. Axiom dice di aver cancellato decine di migliaia di righe costruite su ipotesi non dimostrate e di aver riavviato parti del lavoro [1].

Il 10 ottobre, secondo Axiom, un messaggio nel canale ha annunciato che gli agenti avevano dimostrato che il gruppo Monster è semplice [1]. Lean controlla le deduzioni, mentre gli umani ispezionano l'enunciato finale e le definizioni per confermare che esprimono il teorema voluto [1].

Quali errori hanno trovato gli agenti di IA?

Axiom dice che la maggior parte dei problemi trovati era minore, come errori tipografici, sbagli nelle tabelle o ipotesi omesse [1]. Axiom ha trovato 34 deviazioni notevoli dal testo pubblicato che andavano risolte. Il caso più sostanziale riguardava l'Unbalanced Group Theorem [1][2].

Lì gli agenti hanno trovato controesempi a un'asserzione di chiusura nell'argomento di John Walter del 1986, il che ha lasciato ingiustificato un passo chiave senza confutare il teorema stesso [1]. Un argomento alternativo costruito sulla teoria di Ronald Solomon del 1976 dei 2-componenti massimali è diventato un risultato nuovo, scritto in un paper di 35 pagine [1][2]. Solomon e Richard Lyons, che hanno lavorato alla classificazione originale, sono stati consultati [1].

Qualcuno fuori da Axiom ha controllato la prova?

Non ancora, secondo RuntimeWire [4]. Carina Hong, CEO di Axiom, ha detto a RuntimeWire che nessun gruppo esterno ha ancora ricostruito e verificato la prova. Axiom sta pubblicando gli artefatti di build perché altri possano riprodurla [4].

La pagina GitHub dice che un solo comando di build controlla l'intero progetto, e che Axiom ha usato modifiche pendenti a Lake, lo strumento di build di Lean, per portare il tempo di build sotto le 24 ore [3]. The AI Pin ha raccontato il 27 ottobre le affermazioni separate di OpenAI su nuove scoperte matematiche.

La nostra lettura

Opinione: Controllare una dimostrazione che nessuna persona ha mai letto per intero è un uso più convincente dell'IA in matematica che inseguire nuovi titoli, e trovare 34 deviazioni reali mostra che il controllo aveva mordente. Il risultato è forte solo quanto i controlli esterni, quindi una ricostruzione indipendente e una revisione degli errata da parte della teoria dei gruppi contano più del numero di righe.

Che cosa non abbiamo potuto verificare

• Se la prova di 43.1 milioni di righe si compila e si controlla fuori da Axiom; secondo RuntimeWire, nessun gruppo esterno aveva completato una ricostruzione al 27 ottobre 2026.
• Quali modelli di IA hanno alimentato gli agenti; Axiom dice solo che hanno usato un mix di modelli che cambiava.
• Come giudicano il risultato i teorici dei gruppi indipendenti; al momento della pubblicazione non abbiamo trovato una reazione pubblicata di un teorico dei gruppi fuori dalla cerchia di consulenti di Axiom.
• L'elenco completo delle 34 deviazioni notevoli; Axiom dice che pubblicherà la lista degli errata dopo aver consultato i teorici dei gruppi.
• Se il nuovo paper sull'Unbalanced Group Theorem regge alla peer review; è pubblicato su Hexagon, e non abbiamo potuto confermare alcuna peer review di una rivista.