OpenAI attribuisce a GPT-5.6 Sol Ultra la produzione di una dimostrazione della Cycle Double Cover Conjecture, formalizzata anche nel sistema di verifica Lean, ma la validazione indipendente dei matematici è ancora in corso.

La congettura della doppia copertura ciclica nasce nel cuore della teoria dei grafi, una disciplina che studia strutture matematiche utilizzate per descrivere reti, connessioni e sistemi complessi. Un grafo può essere immaginato come una rete composta da nodi collegati da archi. La condizione “senza ponti” significa che non esiste un singolo collegamento la cui rimozione spezzi la rete in due parti isolate. La domanda posta dalla congettura è apparentemente semplice: ogni rete di questo tipo può essere ricoperta completamente da una collezione di cicli, facendo in modo che ogni arco venga attraversato esattamente due volte?

Dietro questa formulazione quasi infantile si nasconde uno dei problemi più ostinati della matematica moderna. La congettura è stata associata ai lavori di George Szekeres e Paul Seymour negli anni Settanta e per decenni ha resistito agli attacchi dei migliori specialisti di teoria dei grafi. Il motivo è che non basta trovare una configurazione che funzioni per milioni di casi: in matematica una dimostrazione deve valere per ogni possibile struttura ammessa, compresi grafi estremamente irregolari, con archi multipli, componenti disconnesse e configurazioni patologiche che spesso sono il cimitero delle intuizioni umane.

La parte più significativa dell’esperimento non è soltanto il risultato finale, ma il metodo. Secondo la descrizione pubblicata, il sistema ha utilizzato un approccio multi-agente, con numerosi agenti artificiali impegnati contemporaneamente su percorsi matematici differenti: alcuni cercavano costruzioni alternative, altri tentavano di demolire le ipotesi degli altri agenti, altri ancora controllavano la consistenza logica delle dimostrazioni intermedie. È un modello di lavoro molto diverso dalla figura romantica del matematico solitario davanti alla lavagna. È più simile a un laboratorio virtuale dove decine di ricercatori artificiali litigano tra loro senza bisogno di prendere il caffè insieme.

Il dettaglio tecnicamente più importante è la formalizzazione Lean. Una dimostrazione matematica tradizionale può contenere errori nascosti: un passaggio considerato “ovvio”, un caso limite dimenticato, una proprietà utilizzata implicitamente ma non dimostrata. Un sistema come Lean agisce come un revisore estremamente pedante: non accetta intuizioni, eleganza o autorità. Accetta soltanto passaggi formalmente verificabili. Il progetto CDCLean punta proprio a trasformare la dimostrazione in un oggetto controllabile dal kernel del proof assistant, collegando il teorema finale alla formalizzazione del teorema degli otto flussi di Jaeger-Kilpatrick e alla costruzione di un flusso nowhere-zero su Γ = (ZMod 2)^3, da cui viene derivata la copertura ciclica.

Questo cambia profondamente il rapporto tra intelligenza artificiale e ricerca scientifica. Per decenni abbiamo immaginato l’AI come una macchina capace di riconoscere immagini, tradurre lingue o generare testo. Quella fase appare oggi quasi primitiva. Il salto vero è quando un sistema diventa un collaboratore nella frontiera della conoscenza, capace non solo di rispondere ma di esplorare spazi concettuali enormi, produrre ipotesi, verificare errori e trasformare idee vaghe in strutture matematiche rigorose. La nuova frontiera non è più “AI che scrive codice”, ma “AI che partecipa al processo scientifico”.

Naturalmente bisogna evitare il classico entusiasmo da Silicon Valley, dove ogni settimana nasce una nuova “rivoluzione che cambierà tutto entro martedì prossimo”. La storia della tecnologia è piena di promesse gonfiate e di grafici con frecce sempre rivolte verso l’alto. Una dimostrazione generata da un modello linguistico deve essere sottoposta allo stesso livello di critica di una dimostrazione umana. La matematica non concede sconti pubblicitari: un singolo errore logico può cancellare mille pagine di lavoro. La differenza, però, è che questa volta l’AI non ha prodotto solo testo plausibile, ma una struttura formalmente verificabile. Ed è proprio questo elemento a rendere l’evento diverso dalle molte illusioni precedenti.

La conseguenza strategica è enorme. Se questi sistemi riusciranno a dimostrare risultati complessi in modo affidabile, la ricerca scientifica potrebbe trasformarsi in un processo ibrido uomo-macchina. I matematici potrebbero dedicarsi maggiormente alla scelta dei problemi, alla formulazione delle domande e alla comprensione profonda dei risultati, mentre gli agenti artificiali esplorerebbero miliardi di combinazioni logiche impossibili da gestire per un essere umano. Non sarebbe la sostituzione del matematico, ma qualcosa di più sottile: la nascita di un nuovo tipo di scienziato aumentato.