OpenAI e Anthropic hanno presentato, a distanza di circa sei ore, due risultati di ricerca ottenuti attraverso modelli avanzati di intelligenza artificiale che potrebbero confutare l’Exponential Time Hypothesis (ETH), una delle ipotesi fondamentali della teoria della complessità computazionale. Entrambe le aziende hanno indicato il 16 ottobre 2026 come data della scoperta dei rispettivi algoritmi, sviluppati indipendentemente e successivamente accompagnati da dimostrazioni matematiche formalizzate. Anthropic ha reso pubblico il proprio lavoro il 27 ottobre, poco dopo la presentazione da parte di OpenAI di risultati relativi a problemi di matematica, informatica teorica e fisica. Le due ricerche affrontano il problema 3-SAT, una particolare formulazione del problema di soddisfacibilità booleana nella quale occorre stabilire se esista un’assegnazione di valori di verità capace di soddisfare simultaneamente una formula composta da clausole contenenti al massimo tre letterali. Il risultato rivendicato consiste nella costruzione di algoritmi deterministici con complessità temporale subesponenziale rispetto al numero delle variabili, una proprietà che, qualora venisse confermata, contraddirebbe direttamente l’ETH e richiederebbe una revisione di numerosi risultati teorici basati su tale ipotesi.
L’Exponential Time Hypothesis, formulata nel 1999 da Russell Impagliazzo e Ramamohan Paturi, sostiene che il problema 3-SAT non ammetta algoritmi deterministici capaci di risolvere tutte le istanze in tempo subesponenziale rispetto al numero delle variabili. Nella notazione della complessità computazionale, questa condizione viene espressa attraverso il limite 2^o(n), dove n rappresenta il numero delle variabili e o(n) indica una funzione che cresce più lentamente di qualsiasi funzione lineare positiva di n nel limite asintotico. La disponibilità di un algoritmo generale con questa complessità sarebbe quindi incompatibile con l’ipotesi. L’importanza dell’ETH deriva dal suo utilizzo come fondamento di numerose dimostrazioni di limiti inferiori per problemi algoritmici, in particolare nella teoria dei grafi, nell’ottimizzazione combinatoria, nella biologia computazionale e nell’elaborazione delle interrogazioni nei database. Le conseguenze di una sua eventuale confutazione riguarderebbero soprattutto la validità delle dimostrazioni condizionate all’ETH, e non necessariamente l’efficienza pratica degli algoritmi attualmente utilizzati.
Anthropic ha attribuito la scoperta dell’algoritmo centrale a un modello Claude destinato alla ricerca interna, che avrebbe raggiunto il risultato il 16 ottobre senza suggerimenti o interventi umani durante la fase di individuazione della soluzione. Secondo la documentazione pubblicata, il processo ha comportato la generazione di circa 14 milioni di token di output. Successivamente, i ricercatori dell’azienda hanno collaborato con Claude per migliorare l’esposizione e organizzare formalmente i risultati. La ricerca, intitolata A 2^o(n) Time Algorithm for 3-SAT, è stata pubblicata con l’indicazione di Claude come autore e con Anthropic come organizzazione di riferimento. Il lavoro descrive un algoritmo deterministico che non si limita a stabilire se una formula 3-SAT sia soddisfacibile, ma affronta anche il problema più complesso #3-SAT, che richiede di contare esattamente tutte le assegnazioni capaci di soddisfare la formula. La complessità dichiarata è dell’ordine di 2^O(n log log n / √log n), un limite subesponenziale perché il rapporto tra l’esponente e n tende a zero al crescere delle dimensioni del problema. La possibilità di contare le soluzioni, anziché limitarsi a determinarne l’esistenza, estende la portata teorica della costruzione proposta.
Anthropic ha pubblicato anche il codice della formalizzazione matematica realizzata in Lean 4, un assistente alla dimostrazione che permette di esprimere enunciati e argomentazioni matematiche in un linguaggio formale e di sottoporli alla verifica automatica di un kernel logico. La documentazione disponibile nel repository pubblico contiene gli enunciati principali, i collegamenti tra i risultati della ricerca e le corrispondenti formulazioni Lean, oltre alle istruzioni per riprodurre i controlli. È prevista anche una verifica attraverso nanoda, un kernel indipendente, per ridurre la dipendenza da una sola implementazione del verificatore. La presenza di una formalizzazione verificabile rappresenta un elemento rilevante, ma non elimina la necessità di un controllo matematico esterno: la correttezza logica delle dimostrazioni formalizzate deve infatti essere distinta dalla verifica che gli enunciati codificati corrispondano esattamente alle affermazioni formulate nella ricerca. La documentazione segnala inoltre due dichiarazioni prive di dimostrazione nel file Challenge.lean, utilizzate nell’organizzazione di ulteriori controlli e da non confondere automaticamente con un’invalidazione degli enunciati principali.
OpenAI ha presentato in parallelo una propria costruzione algoritmica, anch’essa attribuita a un modello interno di intelligenza artificiale e sviluppata indipendentemente il 16 ottobre. L’azienda ha dichiarato di aver sottoposto il risultato a una formalizzazione in Lean a partire dal giorno successivo. La ricerca riguarda il conteggio esatto delle assegnazioni soddisfacenti di formule booleane a larghezza fissa e comprende risultati con complessità subesponenziale. La documentazione tecnica distingue tuttavia tra il limite temporale più favorevole presentato nel manoscritto e quello effettivamente espresso nella formalizzazione disponibile, che introduce un ulteriore fattore log log n nell’esponente. Le due costruzioni di OpenAI e Anthropic presentano somiglianze nei limiti asintotici dichiarati, ma utilizzano percorsi matematici differenti. La coincidenza della data di scoperta, comunicata da entrambe le aziende, non implica quindi l’identità degli algoritmi o delle relative dimostrazioni, né costituisce di per sé una conferma reciproca della loro correttezza.
Le implicazioni pratiche dei risultati devono essere distinte da quelle teoriche. Un algoritmo subesponenziale può infatti presentare costanti molto elevate e diventare più efficiente dei metodi esistenti soltanto per dimensioni del problema irraggiungibili nella pratica. Anthropic precisa espressamente che la costruzione proposta riguarda il comportamento asintotico della complessità e non dimostra un miglioramento immediato delle prestazioni dei programmi utilizzati per risolvere istanze reali di SAT. Analogamente, la confutazione dell’ETH non equivale alla soluzione del problema P versus NP, che riguarda la possibilità di risolvere in tempo polinomiale problemi le cui soluzioni possono essere verificate efficientemente. Un tempo subesponenziale può continuare a essere molto superiore a un tempo polinomiale. Non è stata inoltre dimostrata alcuna compromissione diretta di specifici sistemi crittografici: l’impatto sulle applicazioni dipenderebbe dalle caratteristiche degli algoritmi coinvolti e dalle proprietà matematiche sulle quali si fondano i diversi schemi di sicurezza.
La verifica indipendente delle due ricerche assume un’importanza particolare per l’ampiezza delle conseguenze scientifiche potenziali. Russell Impagliazzo, Ramamohan Paturi e Ryan Williams, professore al Massachusetts Institute of Technology, sono stati coinvolti nell’organizzazione dell’esame esterno dei risultati. La loro partecipazione non costituisce una certificazione preventiva delle dimostrazioni, che richiedono ancora un’analisi approfondita da parte della comunità scientifica. Qualora gli algoritmi superassero questi controlli, numerosi teoremi che assumono la validità dell’ETH dovrebbero essere riesaminati per determinare quali conclusioni restino dimostrabili attraverso ipotesi alternative e quali limiti algoritmici non siano più sostenibili. Il lavoro di revisione riguarderebbe quindi non soltanto le nuove costruzioni, ma anche le dipendenze teoriche sviluppate in oltre venticinque anni di ricerca sulla complessità computazionale.
La presentazione quasi contemporanea dei risultati evidenzia anche un cambiamento nelle modalità di valutazione dei modelli avanzati di intelligenza artificiale. Le capacità di questi sistemi sono state tradizionalmente confrontate attraverso benchmark di ragionamento, matematica, programmazione e comprensione linguistica, nei quali vengono assegnati punteggi sulla base di problemi con risposte già note. Le ricerche proposte da OpenAI e Anthropic spostano l’attenzione verso la produzione di risultati matematici originali, accompagnati da procedure formali che permettono ad altri ricercatori di esaminare le affermazioni e tentare di riprodurne la verifica. Ryan Williams ha osservato che strumenti capaci di affrontare problemi precedentemente considerati estremamente difficili potrebbero indurre gli studiosi a formulare domande scientifiche di livello ancora superiore. La possibilità di utilizzare modelli AI per esplorare ipotesi, costruire nuovi algoritmi e formalizzare dimostrazioni introduce così un ulteriore ambito di competizione tra i laboratori, nel quale la qualità dei risultati dipenderà non soltanto dalla capacità di produrre una soluzione, ma anche dalla sua correttezza matematica e dalla validazione indipendente.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI)