Diciotto anni di tentativi, e la dimostrazione completa è arrivata durante il terzo giorno di calcolo. Il 6 novembre 2026 la startup Physical Superintelligence (PSI) ha annunciato che un suo sistema di ricerca interno ha dimostrato la congettura di Aaronson-Ambainis, un problema di informatica quantistica aperto dal 2008. Il sistema si basa su un modello di Anthropic che non è pubblico. Lean, un programma che controlla ogni singolo passaggio logico, ha accettato la prova.
Sui tre giorni serve precisione. PSI scrive che il sistema aveva una dimostrazione completa durante il terzo giorno di una sessione di calcolo, quella che in gergo si chiama run. L'azienda non dice quante ore macchina siano servite in totale né quanta potenza di calcolo, e non parla di tre giorni partiti da un foglio bianco.
Tutto parte da un algoritmo del 1994
Per capire di cosa parliamo bisogna tornare a Peter Shor. Nel 1994 ha pubblicato un algoritmo quantistico che scompone numeri grandi molto più in fretta di qualunque metodo noto per i computer tradizionali. Il trucco sta in uno schema che si ripete, nascosto dentro il problema: la periodicità. Shor funziona perché quella struttura c'è.
E se l'input è casuale? Quasi mai un input casuale ha una struttura da sfruttare. Nel 2008 Scott Aaronson e Andris Ambainis hanno formulato una congettura sui polinomi e hanno mostrato che, se fosse vera, sugli input casuali i computer quantistici sarebbero al massimo polinomialmente più veloci di quelli classici. Più veloci, sì. Di un margine che non esplode.
Un'immagine aiuta. Pensa a una fila di milioni di interruttori, ognuno su 0 o su 1, e a una domanda a cui rispondere con sì o no. Il computer classico controlla gli interruttori uno alla volta. Quello quantistico, grazie alla sovrapposizione, può interrogare più posizioni insieme: non le legge tutte gratis, ma organizza le domande in un altro modo. La congettura dice che, in questo scenario, c'è sempre almeno un interruttore che in media pesa abbastanza sul risultato finale.
Il giudice è un software che non fa sconti
Il dettaglio che rende la notizia più solida di tanti annunci sull'IA è Lean. È un proof assistant: la dimostrazione va scritta in un linguaggio formale e il computer verifica ogni passaggio, senza accettare scorciatoie. Se un pezzo non torna, la prova non passa. Qui nessuna IA dà il voto a un'altra IA.
PSI ha messo su GitHub il paper e il codice della formalizzazione. Stando alla documentazione del progetto, la prova è stata verificata con due implementazioni indipendenti del kernel di Lean, senza passaggi lasciati in sospeso e senza assiomi aggiunti.
Poi il sistema ha continuato a lavorare su problemi aperti collegati. Secondo PSI ha migliorato il risultato due volte, e Lean ha accettato anche la versione finale.
Turturean imposta, Halverson controlla
Il lavoro è stato guidato da David Turturean, dello staff tecnico di PSI, che ha impostato il problema e supervisionato la produzione della dimostrazione. Jim Halverson ha partecipato al controllo della prova e Phiala Shanahan ha commentato la formalizzazione in Lean. Quanto abbia pesato l'intervento umano rispetto a quello del modello, PSI non lo quantifica.
La stessa azienda scrive che la dimostrazione poggia su idee di Shachar Lovett e Jiapeng Zhang, di David Reimer e di altri.
Il pezzo di contesto più interessante arriva da Stanford. Ad agosto 2026 Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan avevano dimostrato un caso particolare della congettura, quello degli algoritmi quantistici che leggono l'input in un numero fisso di round paralleli. Secondo PSI, i quattro hanno letto la dimostrazione completa, hanno mandato commenti e stanno scrivendo una versione più breve per gli specialisti. Nell'annuncio di PSI la loro reazione è netta: «È un risultato enorme. Risolve una congettura vecchia di decenni».
Shor resta in piedi
Attenzione a non leggerci più di quello che c'è. Il risultato vale per una classe precisa di problemi, con input privi di struttura, nel cosiddetto modello a interrogazioni: lì un vantaggio quantistico esponenziale non esiste. Dove la struttura c'è, come nei numeri che l'algoritmo di Shor sa scomporre, il discorso resta quello di prima. Chi ne deduce che i computer quantistici non servano più sbaglia lettura.
Poi ci sono le cautele sul metodo. L'annuncio viene dall'azienda che ha fatto il lavoro, senza ancora una revisione paritaria indipendente, e il modello Anthropic usato non ha un nome pubblico. A parte i ricercatori di Stanford citati da PSI, nessun esperto esterno si è ancora espresso.
Il testo di Blanc, Docter, Strassle e Tan non è ancora uscito. Il codice invece è già su GitHub, e chi sa usare Lean può scaricarlo e ricontrollare la prova da sé.
