- Un sistema di intelligenza artificiale sviluppato dall'Università di Peking ha risolto autonomamente la congettura di Anderson, un problema di algebra commutativa rimasto aperto dal 2014, completando l'operazione in circa 80 ore con intervento umano minimo.
- L'architettura si basa su due agenti: Rethlas esplora strategie risolutive attingendo da una libreria di teoremi, mentre Archon trasforma la soluzione nel linguaggio formale Lean 4 per la verifica automatizzata.
- Sebbene il paper non sia ancora sottoposto a peer-review, il risultato dimostra come la ricerca matematica possa essere concretamente automatizzata combinando ragionamento informale e verifica formale.
Un team di ricerca dell’Università di Peking ha presentato un sistema di intelligenza artificiale in grado di risolvere autonomamente problemi matematici avanzati e di verificarne i risultati. Il sistema ha affrontato con successo la congettura di Anderson, un quesito di algebra commutativa rimasto aperto dal 2014, completando l’intera operazione in circa 80 ore di elaborazione. Si tratta di un risultato che apre prospettive inedite sull’automazione della ricerca matematica, un campo tradizionalmente resistente all’intervento delle macchine.
Il caso è interessante perché il processo si è svolto con un intervento umano minimo, segnando una differenza rispetto agli approcci precedenti in cui i matematici dovevano guidare costantemente i software di verifica. Secondo quanto riportato in un paper preliminare pubblicato su arXiv, il sistema ha operato in modo largamente autonomo, dall’esplorazione delle strategie risolutive fino alla formalizzazione finale della dimostrazione.
Un sistema a doppio agente
L’architettura sviluppata dai ricercatori cinesi si basa su due componenti distinti che collaborano tra loro. Il primo, chiamato Rethlas, si occupa di esplorare le possibili strategie per affrontare il problema matematico, attingendo da un motore di ricerca specializzato in teoremi chiamato Matlas. Questo agente lavora in modo simile a come procederebbe un matematico umano, cercando collegamenti tra concetti e formulando ipotesi di dimostrazione.
Il secondo componente, Archon, entra in gioco quando Rethlas produce una potenziale soluzione. Archon trasforma la prova proposta in un formato compatibile con Lean 4, un linguaggio di programmazione e verificatore di teoremi interattivo. Lean 4 dispone di una libreria gestita dalla comunità che contiene centinaia di migliaia di teoremi e definizioni, permettendo al sistema di confrontare e validare ogni passaggio logico.
Come funzionano Rethlas e Archon
Il funzionamento integrato dei due agenti rappresenta un tentativo di colmare il divario tra il ragionamento in linguaggio naturale e la verifica formale automatizzata. I modelli linguistici di grandi dimensioni, pur essendo capaci di generare testi matematici plausibili, tendono a produrre errori e imprecisioni che sfuggono a una validazione rigorosa. Al contrario, i sistemi di verifica formale garantiscono accuratezza assoluta ma richiedono normalmente che un esperto traduca manualmente ogni passaggio nel linguaggio formale richiesto.
Il framework sviluppato dal team cinese permette al sistema di operare in modo autonomo su entrambi i fronti. Rethlas genera ragionamenti esplorativi mentre Archon si occupa della trasformazione formale, utilizzando un altro motore di ricerca chiamato LeanSearch per facilitare il processo. I ricercatori hanno sottolineato che durante la risoluzione del problema non è stato necessario alcun giudizio matematico da parte dell’operatore umano, anche se la presenza di un matematico esperto potrebbe accelerare il lavoro guidando Archon quando necessario.
La congettura di Anderson e i limiti attuali
Il problema risolto dall’intelligenza artificiale è la congettura proposta da Dan Anderson nel 2014, un quesito relativamente specifico nell’ambito dell’algebra commutativa. Pur non trattandosi di uno dei grandi problemi irrisolti della matematica, come l’ipotesi di Riemann o il problema P vs NP, la risoluzione rappresenta comunque un traguardo significativo per l’automazione della ricerca matematica.
Il paper non è ancora stato sottoposto a revisione paritaria, quindi la validazione indipendente dei risultati è ancora in corso. I ricercatori hanno comunque evidenziato che il loro approccio dimostra concretamente come la ricerca matematica possa essere automatizzata in modo sostanziale attraverso l’intelligenza artificiale, con sistemi di ragionamento informale e formale che operano in tandem per produrre risultati verificabili.
Resta da capire se questo metodo possa essere applicato con successo a problemi di maggiore complessità. Le dimostrazioni matematiche richiedono rigore assoluto e anche i lavori scritti da esperti possono contenere errori sottili, per questo la combinazione tra esplorazione creativa e verifica formale potrebbe rappresentare una direzione promettente per il futuro della disciplina.
