ETH e algoritmi sub-esponenziali: cosa sostiene il risultato di OpenAI

L’Exponential Time Hypothesis, o ETH, è una delle ipotesi che permettono agli informatici teorici di ragionare sui limiti degli algoritmi. Il 26 ottobre 2026 OpenAI ha annunciato un risultato che, se corretto, la confuterebbe: un algoritmo deterministico capace di contare in tempo sub-esponenziale le soluzioni di formule booleane in forma k-CNF. Il caso del 3-SAT, problema centrale della complessità, basterebbe a contraddire l’ETH. È una notizia notevole, ma non equivale a un’immediata rivoluzione del software: il risultato è teorico e l’esame da parte della comunità scientifica è ancora in corso.

Che cosa afferma l’Exponential Time Hypothesis

Nel 3-SAT si riceve una formula logica composta da clausole, ciascuna con al massimo tre letterali, e si chiede se esista un’assegnazione di vero e falso che renda vera l’intera formula. L’ETH sostiene che, nel caso peggiore, nessun algoritmo possa risolvere ogni istanza in tempo inferiore a una crescita esponenziale nel numero n di variabili: formalmente, esiste una costante positiva ε tale che non basta un tempo 2^o(n) per tutti i casi.

Questa non è una dimostrazione matematica già acquisita, ma un’ipotesi. È utile perché molte prove di complessità stabiliscono che un problema è difficile a condizione che l’ETH sia vera. L’ipotesi collega così i limiti di SAT a risultati su grafi, geometria computazionale e altri problemi: se viene meno, cade la premessa di quei limiti condizionali, non automaticamente la correttezza logica delle dimostrazioni che li usano.

Il risultato annunciato da OpenAI

OpenAI descrive un algoritmo deterministico che conta esattamente le assegnazioni soddisfacenti di formule k-CNF, per ogni k fissato, con tempo sub-esponenziale e spazio polinomiale. Contare le soluzioni è un compito almeno altrettanto informativo del semplice decidere se una soluzione esista: basta controllare se il conteggio è maggiore di zero per rispondere alla domanda di soddisfacibilità. Applicato al 3-SAT, il limite di tempo dichiarato contraddice la forma standard dell’ETH.

Il manoscritto pubblicato il 25 ottobre presenta, per una formula con n variabili e m clausole, un limite del tipo (n+m)^O(1) · 2^{O(n log log n / √log n)}, con k fissato. L’esponente cresce più lentamente di n, perciò il tempo è sub-esponenziale rispetto al numero di variabili; non è però polinomiale. Per dimensioni realistiche, una funzione sub-esponenziale può comunque diventare enorme. Il lavoro riguarda un confine teorico, non un nuovo risolutore pronto a sostituire i software SAT in uso.

Che cosa aggiunge la formalizzazione in Lean

OpenAI ha reso disponibili il manoscritto, una dimostrazione in linguaggio naturale e una formalizzazione nel sistema Lean. Un proof assistant controlla che i passaggi codificati seguano le regole logiche del sistema e che il teorema formalizzato discenda dalle definizioni e dagli assiomi ammessi. È un controllo importante: riduce il rischio di errori formali nella parte tradotta e rende il materiale ispezionabile, ma non sostituisce la comprensione del metodo né l’esame delle scelte di modellazione e dei collegamenti fra il testo e il codice.

È utile distinguere anche i limiti esatti riportati nei materiali. La documentazione della formalizzazione Lean descrive il conteggio esatto su formule k-CNF canoniche con un esponente O(n(log log n)²/√log n); il manoscritto aggiornato presenta un limite più stretto per le formule con n variabili e m clausole. Non vanno confusi: il repository specifica quale risultato è formalizzato, mentre il manoscritto espone la versione quantitativa aggiornata. OpenAI afferma che il risultato è stato verificato in Lean e ha pubblicato i file perché possano essere controllati; l’azienda stessa ha inoltre annunciato un gruppo esterno incaricato di esaminare e spiegare il lavoro.

Perché non significa che la crittografia sia già a rischio

Una confutazione dell’ETH avrebbe conseguenze rilevanti per la complessità fine-grained, che usa ipotesi come questa per confrontare la difficoltà dei problemi. Non dimostrerebbe, da sola, che P coincide con NP, né fornirebbe un algoritmo veloce per ogni problema NP-completo: il risultato riguarda formule SAT e un tempo che resta potenzialmente molto elevato. Anche la sicurezza crittografica dipende da ipotesi specifiche sui problemi e sugli avversari; non si può dedurre dal solo titolo che gli schemi correnti siano stati violati.

Il passaggio decisivo ora è capire l’algoritmo e verificare indipendentemente che ogni riduzione e ogni stima di complessità corrispondano al risultato formalizzato. OpenAI ha indicato che esperti di complessità guideranno questo lavoro collettivo e che i materiali saranno pubblici. Per chi segue l’informatica, il punto interessante non è proclamare chiusa una disputa decennale, ma osservare se il risultato regge a una lettura approfondita e come cambieranno, eventualmente, le prove che assumono vera l’ETH.