OpenAI afferma che un suo modello interno ha dimostrato falsa l’Exponential Time Hypothesis (ETH), una congettura di teoria della complessità vecchia di 27 anni. L’annuncio è del 26 ottobre 2026 e arriva con un preprint di 67 pagine e una prova formale scritta in Lean, pubblicati su GitHub. Il preprint non è stato sottoposto a revisione paritaria.
Secondo OpenAI, il modello ha trovato la confutazione in linguaggio naturale il 16 ottobre. Il giorno dopo il risultato è stato formalizzato in Lean, il software che controlla ogni passaggio di una dimostrazione con un programma verificatore. Nello stesso annuncio l’azienda presenta altri due risultati dello stesso modello, uno sulla congettura della local smoothing in analisi armonica e uno sull’esistenza della cromodinamica quantistica.
L’ETH sostiene che il problema 3-SAT, cioè stabilire se un insieme di condizioni logiche possa essere soddisfatto tutte insieme, richieda un tempo che cresce in modo esponenziale con le dimensioni dell’input. Centinaia di articoli la usano per concludere che altri problemi, dalla teoria dei grafi ai database fino alla biologia computazionale, non ammettano soluzioni veloci. Se è falsa, alcuni di quei problemi potrebbero averne. OpenAI precisa che trovare gli algoritmi e portarli in pratica richiederà molta ricerca.
Il giorno dopo anche Anthropic ha pubblicato un proprio lavoro, intitolato “A 2^o(n) Time Algorithm for 3-SAT”, di 49 pagine. La prova Lean 4 conta 1.050 moduli ed è stata ricontrollata da un secondo verificatore indipendente. Il testo confuta anche la versione forte della congettura, la SETH. Secondo l’analisi di DataCamp, i due laboratori sono arrivati in modo indipendente a un limite subesponenziale molto simile.
La verifica umana è appena iniziata. OpenAI ha affidato il lavoro a un gruppo guidato da Russell Impagliazzo e Ramamohan Paturi (UC San Diego) e da Ryan Williams (MIT). Williams ha detto che parti della prova sembrano di routine, mentre “due o tre parti dall’aspetto alieno” richiedono ancora un esame attento. Paturi ha raccontato di essere rimasto sorpreso. C’è poi un punto di metodo: Lean conferma che la dimostrazione è valida, ma serve un controllo umano per accertare che l’enunciato formalizzato corrisponda davvero all’ETH. Anthropic stessa ammette che la sua prova è stata scritta e rivista da modelli di IA e che, al momento della pubblicazione, nessuna persona risulta averla controllata.
Cade anche la questione della crittografia, che molti si sono posti: il risultato non risolve il problema P contro NP, e la cifratura in uso resta al sicuro. OpenAI ha promesso di rendere pubblici tutti i dati grezzi e di finanziare una conferenza sul tema.
Nelle prossime settimane si capirà se le prove reggono. Se sì, i teorici dovranno rivedere i risultati di durezza costruiti sull’ETH, e i controlli formali in Lean diventeranno lo strumento standard per fidarsi di dimostrazioni lunghe scritte da macchine.
