PSI riferisce di una dimostrazione della congettura di Aaronson-Ambainis verificata automaticamente

Physical Superintelligence ha annunciato il 6 novembre 2026 che un sistema di ricerca interno, basato su istanze di un modello non pubblico di Anthropic, aveva trovato una dimostrazione della congettura di Aaronson-Ambainis, un problema di calcolo quantistico ancora aperto dal 2008.

Il sistema ha prodotto una dimostrazione completa nel corso del terzo giorno di un’esecuzione sull’infrastruttura proprietaria di PSI, e l’assistente di dimostrazione Lean l’ha accettata. PSI ha quindi assegnato al sistema problemi aperti correlati, e il sistema ha migliorato due volte il risultato prima che Lean accettasse la versione finale. Il manoscritto e la formalizzazione in Lean 4 sono pubblici.

Cosa dice la congettura sugli speedup quantistici

La questione riguarda i casi in cui i computer quantistici possono essere esponenzialmente più veloci delle macchine classiche. L’algoritmo di fattorizzazione di Shor del 1994 dipende dalla struttura: il suo input presenta uno schema ripetitivo che l’algoritmo può sfruttare. Il risultato di PSI affronta il caso opposto, quello di input casuali o privi di struttura, in cui in genere uno schema del genere è assente.

Nel modello a interrogazioni, un algoritmo classico legge un bit per ogni interrogazione, mentre una interrogazione quantistica può distribuirsi in sovrapposizione su molte posizioni dell’input. La spiegazione di PSI collega questo modello ai polinomi: dopo T interrogazioni quantistiche, la probabilità che l’algoritmo risponda sì è un polinomio limitato dei bit dell’input, di grado al massimo 2T. Simulare l’algoritmo quantistico diventa quindi una questione di stimare quel polinomio senza leggere un numero esponenziale di bit dell’input.

Nel loro articolo originale, Scott Aaronson e Andris Ambainis hanno congetturato che ogni polinomio limitato di basso grado abbia una variabile altamente influente. Hanno dimostrato che, assumendo valida la congettura, ogni algoritmo quantistico a T interrogazioni può essere simulato, sulla maggior parte degli input, da un algoritmo classico che effettua un numero di interrogazioni polinomiale in T. Ne consegue una crescita polinomiale, anziché esponenziale, del numero di interrogazioni classiche, per qualsiasi errore di approssimazione fissato e qualsiasi frazione di input esclusi; ciò non esclude vantaggi quantistici esponenziali per problemi dotati di una struttura adeguata.

Formalmente, il repository considera un polinomio reale p di grado al massimo d, i cui valori sull’ipercubo discreto sono compresi tra 0 e 1. Se la sua varianza rispetto a un input uniforme scelto a caso è almeno ε, una coordinata ha un’influenza di almeno (8√15 / (125π⁴)) · ε^(5/2) / d⁶ e, di conseguenza, di almeno (ε/d)⁷. L’influenza è il valore atteso della variazione al quadrato di p quando si inverte il bit di quella coordinata.

Come è stata costruita e verificata la dimostrazione

L’argomentazione segue un piano di Shachar Lovett e Jiapeng Zhang, basato su certificati frazionari e insiemi di livello, ma sostituisce una disuguaglianza che quel piano lasciava come congettura con una nuova disuguaglianza valida per tutte le coppie. Un determinante genera un appaiamento biunivoco delle configurazioni dell’input. Secondo PSI, questo appaiamento va oltre quello, più debole, del Butterfly Lemma di David Reimer, perché limita anche la frequenza con cui le configurazioni appaiate concordano su ciascuna coordinata, un limite necessario per la nuova disuguaglianza.

Il repository suddivide la dimostrazione elementare in quattro parti: ricavare la disuguaglianza per tutte le coppie dal determinante e dalla biiezione, integrarla sugli insiemi di livello, calcolare la media sulle coordinate e stabilire un limite per le righe con un limite puntuale alla sensibilità. Nel loro insieme, questi passaggi producono il limite esplicito sull’influenza.

Secondo la verifica registrata nel repository, lo sviluppo formale non contiene segnaposto per dimostrazioni né assiomi aggiunti. Le sue dichiarazioni sono state rieseguite attraverso il kernel di Lean e lean4lean, un’implementazione indipendente del verificatore di tipi di Lean. In un’esecuzione in ambiente isolato, un programma di confronto basato sui kernel di nanoda e Lean ha accettato i quattro teoremi finali; su una seconda macchina, ha accettato una piccola soluzione corretta e ne ha respinte quattro deliberatamente errate.

Queste verifiche hanno limiti espliciti. Il lettore deve comunque accertarsi che l’enunciato formale corrisponda alla congettura pubblicata. L’articolo in linguaggio naturale non è di per sé verificato automaticamente, mentre il kernel e il compilatore di Lean, le definizioni di Mathlib e le macchine usate per le verifiche restano parte della base fidata.

Ruoli umani e revisione di esperti

David Turturean, membro del personale tecnico di PSI, ha sviluppato e gestito il sistema di ricerca, definito l’ambito del problema, chiesto al modello di preparare una prima bozza, l’ha esaminata ed è responsabile della correttezza dell’articolo. Il repository dichiara che i modelli di IA hanno prodotto gli enunciati matematici, la prima bozza e la formalizzazione in Lean. Jim Halverson ha verificato la dimostrazione e Phiala Shanahan ha commentato la formalizzazione.

L’annuncio fa seguito a un articolo presentato il 19 agosto 2026 da Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan. Questi autori avevano stabilito la conseguenza relativa alla simulazione classica per gli algoritmi quantistici paralleli, dimostrando che un algoritmo a t interrogazioni e d round può essere simulato sulla maggior parte degli input con t^(O(d²)) interrogazioni classiche. PSI afferma che tutti e quattro stanno esaminando la dimostrazione completa, hanno fornito osservazioni e stanno preparando un’esposizione più breve per gli esperti.

Nella valutazione pubblicata da PSI, i ricercatori hanno scritto: «È un risultato enorme. Risolve una congettura vecchia di decenni, con importanti implicazioni per la natura dei problemi che ammettono accelerazioni quantistiche. La dimostrazione si basa su diverse linee di ricerca nell’analisi delle funzioni booleane e nella combinatoria probabilistica, e le estende. Il tutto è riunito in modo piuttosto magico.»

La verifica immediata è insolitamente concreta: kernel indipendenti possono riprodurre l’argomentazione codificata, mentre gli esperti devono ancora confermare che l’enunciato codificato corrisponda alla congettura di Aaronson e Ambainis e valutare le parti dell’articolo che non rientrano in Lean. Questa ripartizione determina che cosa attestano le verifiche automatiche e che cosa richiede ancora una revisione matematica umana.