Un sistema di intelligenza artificiale ha contribuito a risolvere uno dei problemi matematici rimasti aperti più a lungo nell’ambito dell’informatica quantistica. A comunicarlo è Physical Superintelligence (PSI), società che ha sviluppato internamente un sistema di ricerca basato su un modello Anthropic non disponibile pubblicamente.
Il risultato riguarda la congettura di Aaronson-Ambainis, formulata nel 2008 e considerata una questione importante per comprendere quando i computer quantistici possono essere realmente molto più veloci delle macchine tradizionali.
Per capire perché questa dimostrazione sia significativa bisogna partire da una domanda: un computer quantistico è sempre in grado di risolvere un problema molto più velocemente di un computer convenzionale?
La risposta è no. I computer quantistici possono offrire vantaggi enormi in determinate situazioni, ma non è detto che questo accada con qualsiasi problema. Uno degli esempi più conosciuti è l’algoritmo sviluppato da Peter Shor nel 1994, che permette di fattorizzare grandi numeri sfruttando una proprietà matematica chiamata periodicità. In sostanza, l’algoritmo riesce a individuare schemi ripetitivi nascosti nel problema, ottenendo un vantaggio significativo rispetto agli algoritmi classici conosciuti.
Il punto è proprio questo: quanto dipende il vantaggio quantistico dalla presenza di una struttura particolare nel problema da risolvere?
Nel 2008 Scott Aaronson e Andris Ambainis formularono una congettura per affrontare la questione. I due ricercatori ipotizzarono che, quando gli input sono casuali e non presentano particolari regolarità, un computer quantistico non possa ottenere un vantaggio esponenziale rispetto a uno tradizionale in una specifica classe di problemi.
Per comprendere meglio il ragionamento possiamo immaginare una sequenza composta da milioni di interruttori, ognuno dei quali può trovarsi nella posizione 0 oppure 1. Un algoritmo deve analizzare questa sequenza per rispondere a una domanda con due possibili risultati: sì oppure no.
Un computer tradizionale deve consultare gli interruttori uno alla volta. Un computer quantistico, invece, può sfruttare la sovrapposizione degli stati per interrogare più posizioni contemporaneamente, attraverso quella che viene chiamata sovrapposizione quantistica. Questo non significa che possa leggere gratuitamente tutta la sequenza, ma gli permette di organizzare le interrogazioni in maniera differente.
La congettura di Aaronson e Ambainis riguarda proprio le condizioni matematiche che rendono possibile questo vantaggio. Il problema viene ricondotto a una proprietà delle funzioni polinomiali: se il risultato dipende da una funzione costruita a partire dai singoli bit della sequenza e da loro combinazioni, esiste almeno un bit che, mediamente, deve avere un’influenza sufficientemente importante sul risultato.
L’influenza è una misura matematica di quanto cambia il risultato della funzione quando si modifica un singolo bit, passando da 0 a 1 o viceversa. Si può immaginare il risultato come la lancetta di uno strumento: cambiando posizione a un interruttore, la lancetta può spostarsi molto, poco oppure rimanere quasi ferma.
La congettura sostiene che, quando il risultato complessivo varia in modo significativo, almeno uno degli interruttori debba avere un’influenza non trascurabile. Non è quindi possibile che milioni di variabili contribuiscano tutte in maniera infinitesimale, senza che emerga qualche elemento particolarmente significativo.
Dimostrare questa proprietà significa anche fornire uno strumento a un algoritmo classico per imitare il comportamento di quello quantistico. Il computer tradizionale può concentrarsi progressivamente sui bit più influenti, stimando il risultato senza dover esaminare l’intero input. In questo modo, per la classe di problemi considerata, il numero di interrogazioni necessarie cresce al massimo in maniera polinomiale rispetto a quelle richieste dall’algoritmo quantistico, anziché essere esponenzialmente superiore.
La dimostrazione dell’intelligenza artificiale verificata con Lean
Secondo quanto raccontato da PSI, il proprio sistema di ricerca ha individuato una dimostrazione completa durante il terzo giorno di elaborazione. Il lavoro è stato condotto utilizzando infrastruttura interna e istanze di un modello Anthropic non pubblico.
La parte particolarmente interessante è il modo in cui è stata verificata la soluzione. La dimostrazione è stata formalizzata utilizzando Lean, un sistema chiamato proof assistant, progettato per controllare matematicamente ogni singolo passaggio di una dimostrazione.
Non si tratta semplicemente di chiedere a un’altra intelligenza artificiale se un ragionamento appare corretto. Lean verifica che i passaggi rispettino le definizioni, le regole logiche e le ipotesi stabilite, individuando eventuali errori o dimostrando che una conclusione deriva effettivamente dalle premesse.
PSI ha inoltre pubblicato su GitHub il paper e il codice della formalizzazione. Secondo la documentazione del progetto, la dimostrazione è stata verificata anche attraverso due implementazioni indipendenti del kernel di Lean, senza passaggi lasciati in sospeso o assiomi aggiunti al progetto. Il repository include quindi gli strumenti necessari per esaminare e riprodurre le verifiche.
Il lavoro è stato guidato da David Turturean, membro dello staff tecnico di PSI, che ha sviluppato il sistema di ricerca, impostato il problema e supervisionato la produzione della dimostrazione. Jim Halverson ha contribuito all’audit della prova, mentre Phiala Shanahan ha fornito osservazioni sulla formalizzazione in Lean.
La società riferisce inoltre che Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan, ricercatori di Stanford che nell’agosto 2026 avevano già dimostrato un caso particolare della congettura, hanno esaminato la nuova dimostrazione e inviato le proprie osservazioni. I ricercatori stanno preparando una presentazione più breve del risultato destinata alla comunità scientifica.
È importante non confondere questo risultato con la dimostrazione che i computer quantistici non possano più offrire vantaggi significativi. La conclusione è molto più circoscritta: la congettura dimostrata da PSI chiarisce che, per gli specifici problemi considerati e in assenza di particolari strutture negli input, non è possibile ottenere un’accelerazione quantistica esponenziale nel modello di interrogazione studiato.
Resta comunque un risultato matematico rilevante: una questione aperta dal 2008 ha trovato una dimostrazione e, in questo caso, l’intelligenza artificiale ha avuto un ruolo determinante nel percorso che ha portato alla soluzione.