Il teorema più lungo della matematica ora è in Lean
Axiom ha pubblicato il 27 ottobre una dimostrazione completa in Lean della classificazione dei gruppi semplici finiti, considerata la prova più lunga mai scritta: circa 15.000 pagine in oltre 500 articoli, opera di più di cento matematici. Secondo l'azienda, ingegneri e matematici hanno guidato sciami di agenti AI che in 24 giorni l'hanno riscritta in 43,1 milioni di righe di codice, che il computer controlla passaggio per passaggio.
Cosa dice il teorema, in parole semplici
I gruppi descrivono le simmetrie: un cubo, per esempio, si può ruotare in 24 modi senza che cambi aspetto. Ogni gruppo finito si scompone in pezzi indivisibili, i gruppi semplici, come una molecola si scompone in atomi. La classificazione è la loro tavola periodica: gruppi ciclici di ordine primo, gruppi alternanti, 16 famiglie "di tipo Lie" e 26 gruppi sporadici, il più grande dei quali, il Mostro, ha circa 8 × 10^53 elementi. Il difficile non è trovarli, ma dimostrare che non ne esistono altri. Lean è un linguaggio in cui definizioni e dimostrazioni si scrivono in modo così preciso che un programma può controllarne ogni passaggio.
Come hanno lavorato gli agenti
- Si è partiti il 2 ottobre da una mappa della prova divisa in 108 tappe e circa 380 compiti più piccoli.
- Alcuni agenti scomponevano gli argomenti difficili e rivedevano gli enunciati, altri cercavano risultati già esistenti o scrivevano le prove. I matematici si occupavano degli ostacoli veri.
- Il 10 ottobre è arrivata la prova che il Mostro è semplice, il 25 ottobre erano chiuse tutte le tappe.
- La base è Mathlib, più circa 1,2 milioni di righe del progetto Qiuzhen-CFSG.
- Per confronto: nel 2012 il gruppo di Georges Gonthier aveva impiegato sei anni per formalizzare in Coq il solo teorema di Feit-Thompson, che occupa 255 pagine.
Cosa hanno trovato nei libri
Tradurre in Lean obbliga a scrivere ogni passaggio, e così sono venuti fuori errori nella letteratura. Per lo più refusi, tabelle sbagliate o ipotesi dimenticate, ma Axiom conta 34 scostamenti seri. Un lemma dei volumi di Aschbacher e Smith era falso, con un controesempio nel gruppo SL₂(5). Il caso più grosso riguarda l'Unbalanced Group Theorem: nella prova di John Walter del 1986 un passaggio non regge (controesempio costruito su PSL₂(49)). Il teorema resta vero. Gli agenti hanno seguito un'altra strada, basata su un lavoro di Ronald Solomon del 1976, e ne è uscito un risultato nuovo di teoria dei gruppi, descritto in un paper di 35 pagine di Colin Defant e Ken Ono. Dopo, i matematici di Axiom hanno trovato anche una scorciatoia che ne fa a meno. Sono stati consultati Richard Lyons e lo stesso Solomon, tra gli autori della classificazione originale.
Cosa è verificato e cosa no
- Il codice è pubblico su GitHub. Secondo il README non ci sono buchi (
sorry), si usano solo i tre assiomi standard di Lean e nessun calcolo è affidato al compilatore (native_decide). - L'enunciato finale non l'ha scritto Axiom: viene dal progetto indipendente TauCeti ed era già tra i problemi aperti della classifica lean-eval di lean-lang.org. Dice che ogni gruppo semplice finito è uno di quelli della lista.
- Chiunque può ricompilare il progetto, ma per stare sotto le 24 ore di build Axiom ha usato modifiche a Lake non ancora integrate. Al 28 ottobre non risultano verifiche indipendenti e lean-eval non registra ancora soluzioni.
- I numeri (righe, giorni, scostamenti) sono di Axiom. Il nuovo teorema è un preprint non ancora revisionato e l'elenco completo degli errori deve ancora uscire.
Perché conta
La classificazione si usa in algebra, teoria dei numeri, combinatoria e fisica, spesso citata in una riga sola. Ora ogni passaggio ha una forma che una macchina può controllare e altri possono riusare. Per l'AI è uno dei risultati più ambiziosi finora in matematica: gli agenti non risolvono solo problemi da gara, ma traducono decenni di letteratura in matematica verificata e trovano errori nei testi pubblicati. Gli esperti però restano indispensabili, per i punti critici e per controllare che l'enunciato dica davvero quello che deve.
