The Pulse
Axiom formalizza la classificazione dei gruppi semplici finiti, una dimostrazione di 15.000 pagine
Axiom afferma che i suoi team di agenti di IA hanno contribuito a produrre in 24 giorni una formalizzazione in Lean della classificazione dei gruppi semplici finiti, composta da 43,1 milioni di righe. Il lavoro ha anche portato alla luce er
AI.info Team · Scritto con l’IA · verificato ·
Il 26 ottobre Axiom ha annunciato di aver trasformato la classificazione dei gruppi semplici finiti in una dimostrazione in Lean verificabile al computer: un progetto che, secondo l’azienda, ha richiesto 24 giorni e prodotto circa 43,1 milioni di righe di codice. Il teorema, noto come CFSG, descrive gli elementi fondamentali dei gruppi finiti: un risultato matematico la cui dimostrazione originale si estende per circa 15.000 pagine, oltre 500 articoli e il lavoro di circa 100 matematici.
Una dimostrazione ricostruita a partire da centinaia di articoli
I gruppi finiti descrivono sistemi di simmetrie. La CFSG afferma che ogni gruppo semplice finito appartiene a un elenco definito: gruppi ciclici di ordine primo, gruppi alterni, sedici famiglie infinite di gruppi di tipo Lie oppure uno dei 26 gruppi sporadici. Per dimostrare che l’elenco è completo, generazioni di matematici hanno dovuto costruire e collegare risultati sparsi in un’ampia letteratura.
L’annuncio di Axiom riguarda la formalizzazione di questa classificazione già nota, non la scoperta della classificazione stessa. L’azienda afferma che i suoi ingegneri e matematici hanno diretto sciami di agenti di IA nella traduzione della dimostrazione di prima generazione in Lean, un linguaggio in cui un assistente alla dimostrazione può verificare ogni deduzione. La pagina pubblica del progetto riporta 43,1 milioni di righe di Lean, 2,05 milioni di dichiarazioni e 715 articoli e libri usati come fonti; l’azienda afferma che la formalizzazione si basa su precedenti lavori in Lean, tra cui circa 1,2 milioni di righe del progetto Qiuzhen-CFSG.
Gli agenti si sono divisi il lavoro; le persone hanno verificato l’obiettivo
Axiom ha aperto un canale Slack per coordinare il progetto il 1° ottobre, poi ha avviato il suo primo sciame di agenti il 2 ottobre. Una mappa interna della dimostrazione ha suddiviso il lavoro in 108 traguardi e circa 380 compiti più piccoli. Secondo l’azienda, gli agenti responsabili hanno scomposto le dimostrazioni più difficili e riesaminato gli enunciati da formalizzare, mentre altri agenti cercavano risultati già esistenti o scrivevano dimostrazioni in Lean; i matematici hanno esaminato gli ostacoli matematici, mentre gli ingegneri mantenevano il sistema condiviso.
Il piano iniziale non ha retto per tutta la durata del progetto. Axiom afferma che alcuni compiti dipendevano da premesse che gli agenti avevano dato per vere anziché dimostrare, inducendo il team a scartare decine di migliaia di righe e a ricominciare parti del lavoro. Lean può verificare che una deduzione formale discenda dalle sue premesse, ma chi supervisiona un progetto deve comunque controllare che l’enunciato formale e le definizioni esprimano il teorema voluto. Axiom afferma che i suoi revisori hanno esaminato questa specifica, mentre Lean verificava le deduzioni.
Un difetto in una dimostrazione pubblicata dell’Unbalanced Group Theorem
La formalizzazione della letteratura ha anche rivelato un problema in una dimostrazione pubblicata dell’Unbalanced Group Theorem, un risultato usato in una parte considerevole della classificazione. Axiom afferma che i suoi agenti hanno trovato controesempi a un’affermazione di chiusura nella trattazione di John Walter del 1986. L’azienda precisa esplicitamente che questi controesempi non hanno confutato l’Unbalanced Group Theorem: hanno lasciato senza giustificazione un passaggio di quella particolare via dimostrativa.
In un articolo pubblicato il 27 ottobre, Colin Defant e Ken Ono precisano la portata del problema: «Questo ostacolo riguarda quella particolare dimostrazione. L’UGT ha anche altre dimostrazioni». Colin Defant e Ken Ono, «The Unbalanced Group Theorem»
Axiom afferma che i teorici dei gruppi Richard Lyons e Ronald Solomon hanno fornito consulenza sul problema e che la dimostrazione alternativa si è basata sul lavoro di Solomon del 1976. AxiomProver ha prodotto e formalizzato un nuovo risultato chiamato «Preservation of simple tops» per questa via dimostrativa. L’articolo che accompagna il progetto documenta anche una deduzione più breve, trovata dai matematici di Axiom dopo la formalizzazione, che raggiunge la conclusione necessaria senza quel nuovo teorema.
Il codice è pubblico; l’elenco degli errata è ancora in preparazione
Axiom ha reso disponibile la formalizzazione attraverso un repository GitHub pubblico e una mappa interattiva della dimostrazione. Il repository descrive il lavoro come una dimostrazione in Lean 4 «senza sorry», costruita su Mathlib e TauCeti e basata sugli assiomi standard di Lean. Questo permette ad altri ricercatori di esaminare il codice e compilare il progetto, mentre l’enunciato esatto del teorema formalizzato resta qualcosa che le persone devono valutare.
Il progetto registra anche 34 «scostamenti degni di nota» rispetto a quanto pubblicato che, secondo Axiom, hanno richiesto una soluzione; molte altre segnalazioni riguardavano refusi, errori nelle tabelle, ipotesi omesse o passaggi ricostruibili dal contesto. L’azienda afferma di stare preparando con i teorici dei gruppi un elenco dettagliato degli errata, e la pagina del progetto indica che l’elenco è ancora in preparazione. La pubblicazione di Axiom rende quindi disponibile per l’esame una dimostrazione formale di notevole portata, ma il resoconto pubblico delle correzioni non è ancora completo.