L'AI mette alla prova una delle più grandi dimostrazioni della matematica in un progetto dell'azienda Axiom

Per capire la portata del risultato bisogna partire da una domanda apparentemente semplice: che cosa sono i gruppi semplici finiti? In matematica, un gruppo è una struttura che permette di descrivere operazioni e simmetrie. Un esempio intuitivo è un cubo, che può essere ruotato in 24 modi diversi mantenendo invariata la sua forma. Queste rotazioni possono essere combinate tra loro seguendo regole precise. I gruppi semplici finiti rappresentano, in un certo senso, gli elementi fondamentali con cui si possono costruire strutture matematiche più complesse. La classificazione dimostra che tutti questi gruppi appartengono a un elenco ben definito, composto da alcune famiglie infinite e da 26 gruppi eccezionali, chiamati sporadici. Il problema non consisteva soltanto nell’individuare questi elementi, ma nel dimostrare che non ne esistessero altri al di fuori dell’elenco. La dimostrazione ha richiesto il contributo di oltre cento matematici e si è sviluppata attraverso generazioni di ricercatori.

La novità è il metodo utilizzato per verificare questo patrimonio scientifico. Axiom ha impiegato Lean, un sistema informatico che permette di scrivere teoremi e dimostrazioni in un linguaggio rigoroso, controllabile da un computer. Non si tratta di chiedere a un chatbot se una formula sia corretta. Il sistema verifica che ogni passaggio logico discenda dalle definizioni e dalle ipotesi dichiarate. Se manca una condizione necessaria, oppure un risultato viene utilizzato senza essere stato dimostrato, la catena della dimostrazione non può essere considerata completa. Per portare a termine il lavoro, l’azienda ha suddiviso il progetto in 108 traguardi e circa 380 attività più piccole, affidandole a decine di agenti AI. Alcuni si sono concentrati sulla scrittura delle dimostrazioni, altri sulla ricerca dei risultati già disponibili e altri ancora sul coordinamento e sull’integrazione del lavoro. Il gruppo ha riutilizzato anche circa 1,2 milioni di righe provenienti da un progetto precedente, oltre alla biblioteca matematica Mathlib. Le 43,1 milioni di righe prodotte non equivalgono quindi a 43 milioni di nuove scoperte, ma costituiscono la formalizzazione di una vasta rete di conoscenze già esistenti.

Uno degli aspetti più sorprendenti è che la traduzione in un linguaggio verificabile ha portato alla luce problemi in alcuni passaggi della letteratura matematica. Axiom riferisce di aver individuato 34 deviazioni significative rispetto alle dimostrazioni pubblicate, oltre a errori minori come refusi, tabelle imprecise e ipotesi omesse. Il caso più importante riguarda un passaggio della dimostrazione del cosiddetto Unbalanced Group Theorem, contenuto in un lavoro del matematico John Walter del 1986. Gli agenti hanno trovato controesempi a un’affermazione intermedia utilizzata nell’argomentazione. Questo non significa che sia stata smentita la classificazione dei gruppi semplici finiti. Il problema riguardava un passaggio della dimostrazione, non il risultato finale. Per superare l’ostacolo, Axiom ha sviluppato un percorso alternativo basato anche su idee matematiche precedenti, con il contributo e la consulenza di specialisti come Richard Lyons e Ronald Solomon. L’azienda afferma che il lavoro ha prodotto anche un nuovo risultato nell’ambito della teoria dei gruppi. La lista completa delle correzioni e delle differenze individuate è destinata a essere condivisa con la comunità scientifica.

Il risultato va comunque letto con prudenza. La verifica eseguita da Lean e la verifica indipendente dell’intero progetto sono due cose diverse. Il codice è pubblico su GitHub, ma al 28 ottobre 2026, secondo la testata Times of AI, nessun gruppo esterno aveva ancora ricostruito e controllato autonomamente l’intera dimostrazione. Gli esperti dovranno accertare non soltanto che il codice venga eseguito correttamente, ma anche che l’enunciato formalizzato corrisponda esattamente al teorema matematico che si intende dimostrare. È una distinzione fondamentale, perché un sistema può verificare perfettamente una conclusione che discende dalle ipotesi inserite nel programma, senza poter stabilire da solo se quelle ipotesi rappresentino correttamente il problema originale. Axiom sostiene di aver completato la dimostrazione e ha messo a disposizione gli strumenti per consentire controlli esterni. Il risultato è quindi verificabile in linea di principio, ma la sua riproduzione indipendente resta un passaggio decisivo per consolidarne l’affidabilità.

Al di là della singola impresa, la vicenda suggerisce un possibile cambiamento nel rapporto tra AI e ricerca scientifica. Questi sistemi potrebbero aiutare gli studiosi a esplorare dimostrazioni complesse, controllare risultati precedenti e individuare errori difficili da riconoscere nella lettura di migliaia di pagine. La stessa impostazione potrebbe essere utile in altri campi nei quali la correttezza formale è essenziale, come la verifica del software e dei chip elettronici. Ma non siamo ancora davanti a macchine capaci di sostituire autonomamente i matematici. Il progetto ha richiesto competenze umane per definire il problema, organizzare il lavoro, interpretare i controesempi e scegliere nuove strategie quando una strada si è rivelata insufficiente. Il valore dell’AI, in questo caso, consiste soprattutto nella capacità di coordinare un’enorme quantità di attività e rendere controllabili passaggi che prima erano distribuiti in una letteratura difficile da esaminare nel suo insieme. La vera svolta non è che una macchina abbia riscritto in poche settimane decenni di matematica, ma che strumenti AI e verificatori formali possano rendere più controllabile il sapere scientifico. Saranno però il confronto con la comunità e le verifiche indipendenti a stabilire fino a che punto questa promessa sia stata mantenuta.