GPT-5.6 Sol Ultra ha prodotto una dimostrazione completa della Cycle Double Cover Conjecture, uno dei problemi aperti più longevi della teoria dei grafi. La prova è stata pubblicata insieme al prompt utilizzato e a una formalizzazione realizzata con Lean 4, così da permettere ai matematici di esaminare sia il ragionamento sia la sua traduzione in un sistema di verifica formale. Il risultato deve ancora superare il controllo indipendente della comunità scientifica e non può quindi essere considerato definitivamente acquisito.
La congettura riguarda i grafi non orientati privi di ponti, cioè grafi nei quali la rimozione di un singolo arco non provoca la separazione di una componente connessa. L’enunciato sostiene che, per ogni grafo di questo tipo, sia possibile costruire una collezione di cicli nella quale ciascun arco compaia esattamente due volte. Sebbene la formulazione sia relativamente semplice, il problema resiste dagli anni Settanta e comprende una vasta classe di strutture, inclusi multigrafi con archi paralleli.
La dimostrazione proposta parte da una riduzione standard ai grafi cubici, nei quali ogni vertice è incidente a tre archi. Su questa struttura viene utilizzata l’esistenza di un flusso non nullo sullo spazio vettoriale tridimensionale (\mathbb{F}_2^3), equivalente all’impiego di un flusso a otto valori. A ogni arco vengono quindi associate coppie di elementi del gruppo, costruite in modo che, presso ciascun vertice, ogni elemento compaia zero oppure due volte.
Questa proprietà locale consente di definire, per ogni elemento del gruppo, un sottografo nel quale tutti i vertici hanno grado zero o due. Ogni sottografo è quindi formato da un’unione di cicli. Poiché ogni arco appartiene esattamente a due delle coppie assegnate, l’insieme complessivo dei cicli ottenuti copre ciascun arco due volte, soddisfacendo la condizione richiesta dalla congettura.
Il passaggio più delicato consiste nel rendere compatibili le assegnazioni effettuate localmente ai due estremi di ogni arco. La prova traduce questa compatibilità in un sistema lineare su campi finiti e dimostra che il sistema possiede sempre una soluzione attraverso un argomento di dualità. In questo modo, una costruzione inizialmente valida soltanto intorno ai singoli vertici viene trasformata in un’assegnazione coerente sull’intero grafo.
Il risultato è stato ottenuto attraverso un’architettura multi-agente che permette al modello di distribuire il problema tra numerosi processi di ragionamento paralleli. Gli agenti hanno potuto esplorare formulazioni differenti, sviluppare lemmi intermedi, cercare controesempi e sottoporre le soluzioni candidate a controlli avversariali, mentre un agente principale coordinava e integrava i contributi. Il prompt prescriveva esplicitamente l’impiego dinamico di un massimo di 64 agenti e imponeva di non restituire semplici riduzioni o progressi parziali.
La pubblicazione della prova in linguaggio matematico e della relativa versione Lean rappresenta un elemento essenziale. La verifica formale può controllare la correttezza dei singoli passaggi logici rispetto agli assiomi e alle definizioni implementate, ma non sostituisce completamente la valutazione matematica indipendente. Devono essere esaminate la correttezza delle riduzioni utilizzate, la corrispondenza tra dimostrazione informale e codice, l’assenza di ipotesi nascoste e la validità dei risultati teorici richiamati.
La rilevanza del caso dipende quindi non soltanto dall’eventuale soluzione della congettura, ma dal metodo con cui il risultato è stato prodotto e reso verificabile. Un modello commerciale ha affrontato un problema di ricerca attraverso decomposizione multi-agente, ragionamento simbolico, algebra lineare su campi finiti e formalizzazione assistita. La valutazione definitiva spetta ora agli specialisti di teoria dei grafi e di verifica formale, che dovranno stabilire se la costruzione proposta risolve effettivamente il problema in tutta la sua generalità.